Theorem ifptreq ≪ | index | src | ≫ 

theorem ifptreq (G a p p0 p1 q0 q1: wff):
  $ G -> (p <-> ifp a p0 p1) $ >
  $ G /\ a -> (p0 <-> q0) $ >
  $ G /\ ~a -> (p1 <-> q1) $ >
  $ G -> (p <-> ifp a q0 q1) $;
StepHypRefExpression
1 hyp h 
G -> (p <-> ifp a p0 p1)
2 ifpeq2a 
(a -> (p0 <-> q0)) -> (ifp a p0 p1 <-> ifp a q0 p1)
3 hyp h0 
G /\ a -> (p0 <-> q0)
4 3 exp 
G -> a -> (p0 <-> q0)
5 2, 4 syl 
G -> (ifp a p0 p1 <-> ifp a q0 p1)
6 ifpeq3a 
(~a -> (p1 <-> q1)) -> (ifp a q0 p1 <-> ifp a q0 q1)
7 hyp h1 
G /\ ~a -> (p1 <-> q1)
8 7 exp 
G -> ~a -> (p1 <-> q1)
9 6, 8 syl 
G -> (ifp a q0 p1 <-> ifp a q0 q1)
10 5, 9 bitrd 
G -> (ifp a p0 p1 <-> ifp a q0 q1)
11 1, 10 bitrd 
G -> (p <-> ifp a q0 q1)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)