theorem ifpeq2a (a1 a2 b p: wff): $ (p -> (a1 <-> a2)) -> (ifp p a1 b <-> ifp p a2 b) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aneq2a | (p -> (a1 <-> a2)) -> (p /\ a1 <-> p /\ a2) |
|
| 2 | 1 | oreq1d | (p -> (a1 <-> a2)) -> (p /\ a1 \/ ~p /\ b <-> p /\ a2 \/ ~p /\ b) |
| 3 | 2 | conv ifp | (p -> (a1 <-> a2)) -> (ifp p a1 b <-> ifp p a2 b) |