Theorem bibi12d 234

Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbi12d.1	|- ( ph -> ( ps <-> ch ) )
imbi12d.2	|- ( ph -> ( th <-> ta ) )

Assertion

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

Proof of Theorem bibi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	bibi1d 232	. 2 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	bibi2d 231	. 2 |- ( ph -> ( ( ch <-> th ) <-> ( ch <-> ta ) ) )
5	2, 4	bitrd 187	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )

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:  pm5.32  448  bi2bian9  597  cleqh  2239  abbi  2253  cleqf  2305  vtoclb  2743  vtoclbg  2747  ceqsexg  2813  elabgf  2826  reu6  2873  ru  2908  sbcbig  2955  sbcne12g  3020  sbcnestgf  3051  preq12bg  3700  nalset  4058  undifexmid  4117  exmidsssn  4125  exmidsssnc  4126  exmidundif  4129  opthg  4160  opelopabsb  4182  wetriext  4491  opeliunxp2  4679  resieq  4829  elimasng  4907  cbviota  5093  iota2df  5112  fnbrfvb  5462  fvelimab  5477  fmptco  5586  fsng  5593  fressnfv  5607  funfvima3  5651  isorel  5709  isocnv  5712  isocnv2  5713  isotr  5717  ovg  5909  caovcang  5932  caovordg  5938  caovord3d  5941  caovord  5942  opeliunxp2f  6135  dftpos4  6160  ecopovsym  6525  ecopovsymg  6528  xpf1o  6738  nneneq  6751  supmoti  6880  supsnti  6892  isotilem  6893  isoti  6894  ltanqg  7208  ltmnqg  7209  elinp  7282  prnmaxl  7296  prnminu  7297  ltasrg  7578  axpre-ltadd  7694  zextle  9142  zextlt  9143  xlesubadd  9666  rexfiuz  10761  climshft  11073  dvdsext  11553  ltoddhalfle  11590  halfleoddlt  11591  bezoutlemmo  11694  bezoutlemeu  11695  bezoutlemle  11696  bezoutlemsup  11697  dfgcd3  11698  dvdssq  11719  rpexp  11831  xmeteq0  12528  comet  12668  dedekindeulemuub  12764  dedekindeulemloc  12766  dedekindicclemuub  12773  dedekindicclemloc  12775  bj-nalset  13093  bj-d0clsepcl  13123  bj-nn0sucALT  13176