Theorem rbida ≪ | index | src | ≫ 

theorem rbida (a b c d: wff):
  $ a /\ c -> b $ >
  $ a /\ d -> b $ >
  $ a /\ b -> (c <-> d) $ >
  $ a -> (c <-> d) $;
StepHypRefExpression
1 bian2a 
(c -> b) -> (c /\ b <-> c)
2 hyp h1 
a /\ c -> b
3 1, 2 syla 
a -> (c /\ b <-> c)
4 aneq1a 
(b -> (c <-> d)) -> (c /\ b <-> d /\ b)
5 hyp h 
a /\ b -> (c <-> d)
6 4, 5 syla 
a -> (c /\ b <-> d /\ b)
7 bian2a 
(d -> b) -> (d /\ b <-> d)
8 hyp h2 
a /\ d -> b
9 7, 8 syla 
a -> (d /\ b <-> d)
10 6, 9 bitrd 
a -> (c /\ b <-> d)
11 3, 10 bitr3d 
a -> (c <-> d)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)