Theorem rbid ≪ | index | src | ≫ 

theorem rbid (a b c: wff):
  $ b -> a $ >
  $ c -> a $ >
  $ a -> (b <-> c) $ >
  $ b <-> c $;
StepHypRefExpression
1 bitr3 
(b /\ a <-> b) -> (b /\ a <-> c) -> (b <-> c)
2 bian2a 
(b -> a) -> (b /\ a <-> b)
3 hyp h1 
b -> a
4 2, 3 ax_mp 
b /\ a <-> b
5 1, 4 ax_mp 
(b /\ a <-> c) -> (b <-> c)
6 bitr 
(b /\ a <-> c /\ a) -> (c /\ a <-> c) -> (b /\ a <-> c)
7 aneq1a 
(a -> (b <-> c)) -> (b /\ a <-> c /\ a)
8 hyp h 
a -> (b <-> c)
9 7, 8 ax_mp 
b /\ a <-> c /\ a
10 6, 9 ax_mp 
(c /\ a <-> c) -> (b /\ a <-> c)
11 bian2a 
(c -> a) -> (c /\ a <-> c)
12 hyp h2 
c -> a
13 11, 12 ax_mp 
c /\ a <-> c
14 10, 13 ax_mp 
b /\ a <-> c
15 5, 14 ax_mp 
b <-> c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)