Theorem bibi12d 235

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 233	. 2 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	bibi2d 232	. 2 |- ( ph -> ( ( ch <-> th ) <-> ( ch <-> ta ) ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.32  457  bi2bian9  616  cleqh  2338  abbibcom  2352  abbib  2356  cleqf  2417  cbvreuvw  2792  vtoclb  2880  vtoclbg  2884  ceqsexg  2954  elabgf  2968  reu6  3015  ru  3050  sbcbig  3098  sbcne12g  3165  sbcnestgf  3199  preq12bg  3898  nalset  4265  undifexmid  4332  exmidsssn  4341  exmidsssnc  4342  exmidundif  4345  opthg  4380  opelopabsb  4404  wetriext  4726  opeliunxp2  4922  resieq  5075  elimasng  5158  cbviota  5345  iota2df  5366  fnbrfvb  5744  fvelimab  5762  fmptco  5877  fsng  5884  fressnfv  5905  funfvima3  5955  isorel  6017  isocnv  6020  isocnv2  6021  isotr  6025  ovg  6231  caovcang  6254  caovordg  6260  caovord3d  6263  caovord  6264  uchoice  6375  opeliunxp2f  6513  dftpos4  6538  ecopovsym  6909  ecopovsymg  6912  xpf1o  7148  nneneq  7162  supmoti  7339  supsnti  7351  isotilem  7352  isoti  7353  ltanqg  7773  ltmnqg  7774  elinp  7847  prnmaxl  7861  prnminu  7862  ltasrg  8143  axpre-ltadd  8259  zextle  9748  zextlt  9749  xlesubadd  10302  rexfiuz  11777  climshft  12095  dvdsext  12647  ltoddhalfle  12685  halfleoddlt  12686  bezoutlemmo  12808  bezoutlemeu  12809  bezoutlemle  12810  bezoutlemsup  12811  dfgcd3  12812  dvdssq  12833  rpexp  12957  pcdvdsb  13128  isnsg  14064  nsgbi  14066  elnmz  14070  nmzbi  14071  nmznsg  14075  gsumcom2fi  14275  islidlm  14925  xmeteq0  15585  comet  15725  dedekindeulemuub  15843  dedekindeulemloc  15845  dedekindicclemuub  15852  dedekindicclemloc  15854  logltb  16104  eupth2lem3lem6fi  16917  bj-nalset  17126  bj-d0clsepcl  17156  bj-nn0sucALT  17209  ltlenmkv  17327