Theorem bibi2d 231

Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypothesis

Ref	Expression
imbid.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
bibi2d	|- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )

Proof of Theorem bibi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . . . 5 |- ( ph -> ( ps <-> ch ) )
2	1	pm5.74i 179	. . . 4 |- ( ( ph -> ps ) <-> ( ph -> ch ) )
3	2	bibi2i 226	. . 3 |- ( ( ( ph -> th ) <-> ( ph -> ps ) ) <-> ( ( ph -> th ) <-> ( ph -> ch ) ) )
4		pm5.74 178	. . 3 |- ( ( ph -> ( th <-> ps ) ) <-> ( ( ph -> th ) <-> ( ph -> ps ) ) )
5		pm5.74 178	. . 3 |- ( ( ph -> ( th <-> ch ) ) <-> ( ( ph -> th ) <-> ( ph -> ch ) ) )
6	3, 4, 5	3bitr4i 211	. 2 |- ( ( ph -> ( th <-> ps ) ) <-> ( ph -> ( th <-> ch ) ) )
7	6	pm5.74ri 180	1 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi1d  232  bibi12d  234  biantr  947  bimsc1  958  eujust  2021  euf  2024  ceqex  2857  reu6i  2921  axsep2  4108  zfauscl  4109  copsexg  4229  euotd  4239  cnveq0  5067  iotaval  5171  iota5  5180  eufnfv  5726  isoeq1  5780  isoeq3  5782  isores2  5792  isores3  5794  isotr  5795  isoini2  5798  riota5f  5833  caovordg  6020  caovord  6024  dfoprab4f  6172  frecabcl  6378  nnaword  6490  xpf1o  6822  ltanqg  7362  ltmnqg  7363  ltasrg  7732  axpre-ltadd  7848  prmdvdsexp  12102  bdsep2  13921  bdzfauscl  13925