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 ) ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.32  453  bi2bian9  612  cleqh  2331  abbi  2345  cleqf  2399  cbvreuvw  2773  vtoclb  2861  vtoclbg  2865  ceqsexg  2934  elabgf  2948  reu6  2995  ru  3030  sbcbig  3078  sbcne12g  3145  sbcnestgf  3179  preq12bg  3856  nalset  4219  undifexmid  4283  exmidsssn  4292  exmidsssnc  4293  exmidundif  4296  opthg  4330  opelopabsb  4354  wetriext  4675  opeliunxp2  4870  resieq  5023  elimasng  5104  cbviota  5291  iota2df  5312  fnbrfvb  5684  fvelimab  5702  fmptco  5813  fsng  5820  fressnfv  5841  funfvima3  5888  isorel  5949  isocnv  5952  isocnv2  5953  isotr  5957  ovg  6161  caovcang  6184  caovordg  6190  caovord3d  6193  caovord  6194  uchoice  6300  opeliunxp2f  6404  dftpos4  6429  ecopovsym  6800  ecopovsymg  6803  xpf1o  7030  nneneq  7043  supmoti  7192  supsnti  7204  isotilem  7205  isoti  7206  ltanqg  7620  ltmnqg  7621  elinp  7694  prnmaxl  7708  prnminu  7709  ltasrg  7990  axpre-ltadd  8106  zextle  9571  zextlt  9572  xlesubadd  10118  rexfiuz  11567  climshft  11882  dvdsext  12434  ltoddhalfle  12472  halfleoddlt  12473  bezoutlemmo  12595  bezoutlemeu  12596  bezoutlemle  12597  bezoutlemsup  12598  dfgcd3  12599  dvdssq  12620  rpexp  12743  pcdvdsb  12911  isnsg  13807  nsgbi  13809  elnmz  13813  nmzbi  13814  nmznsg  13818  islidlm  14512  xmeteq0  15102  comet  15242  dedekindeulemuub  15360  dedekindeulemloc  15362  dedekindicclemuub  15369  dedekindicclemloc  15371  logltb  15617  eupth2lem3lem6fi  16341  bj-nalset  16541  bj-d0clsepcl  16571  bj-nn0sucALT  16624  ltlenmkv  16726