Theorem ifpan2 ≪ | index | src | ≫ 

theorem ifpan2 (a b c p: wff): $ c /\ ifp p a b <-> ifp p (c /\ a) (c /\ b) $;
StepHypRefExpression
1 bitr 
(c /\ ifp p a b <-> c /\ (p /\ a) \/ c /\ (~p /\ b)) ->
  (c /\ (p /\ a) \/ c /\ (~p /\ b) <-> ifp p (c /\ a) (c /\ b)) ->
  (c /\ ifp p a b <-> ifp p (c /\ a) (c /\ b))
2 andi 
c /\ (p /\ a \/ ~p /\ b) <-> c /\ (p /\ a) \/ c /\ (~p /\ b)
3 2 conv ifp 
c /\ ifp p a b <-> c /\ (p /\ a) \/ c /\ (~p /\ b)
4 1, 3 ax_mp 
(c /\ (p /\ a) \/ c /\ (~p /\ b) <-> ifp p (c /\ a) (c /\ b)) -> (c /\ ifp p a b <-> ifp p (c /\ a) (c /\ b))
5 oreq 
(c /\ (p /\ a) <-> p /\ (c /\ a)) -> (c /\ (~p /\ b) <-> ~p /\ (c /\ b)) -> (c /\ (p /\ a) \/ c /\ (~p /\ b) <-> p /\ (c /\ a) \/ ~p /\ (c /\ b))
6 5 conv ifp 
(c /\ (p /\ a) <-> p /\ (c /\ a)) -> (c /\ (~p /\ b) <-> ~p /\ (c /\ b)) -> (c /\ (p /\ a) \/ c /\ (~p /\ b) <-> ifp p (c /\ a) (c /\ b))
7 anlass 
c /\ (p /\ a) <-> p /\ (c /\ a)
8 6, 7 ax_mp 
(c /\ (~p /\ b) <-> ~p /\ (c /\ b)) -> (c /\ (p /\ a) \/ c /\ (~p /\ b) <-> ifp p (c /\ a) (c /\ b))
9 anlass 
c /\ (~p /\ b) <-> ~p /\ (c /\ b)
10 8, 9 ax_mp 
c /\ (p /\ a) \/ c /\ (~p /\ b) <-> ifp p (c /\ a) (c /\ b)
11 4, 10 ax_mp 
c /\ ifp p a b <-> ifp p (c /\ a) (c /\ b)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)