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  942  bimsc1  953  eujust  2016  euf  2019  ceqex  2853  reu6i  2917  axsep2  4101  zfauscl  4102  copsexg  4222  euotd  4232  cnveq0  5060  iotaval  5164  iota5  5173  eufnfv  5715  isoeq1  5769  isoeq3  5771  isores2  5781  isores3  5783  isotr  5784  isoini2  5787  riota5f  5822  caovordg  6009  caovord  6013  dfoprab4f  6161  frecabcl  6367  nnaword  6479  xpf1o  6810  ltanqg  7341  ltmnqg  7342  ltasrg  7711  axpre-ltadd  7827  prmdvdsexp  12080  bdsep2  13768  bdzfauscl  13772