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  5840  funfvima3  5887  isorel  5948  isocnv  5951  isocnv2  5952  isotr  5956  ovg  6160  caovcang  6183  caovordg  6189  caovord3d  6192  caovord  6193  uchoice  6299  opeliunxp2f  6403  dftpos4  6428  ecopovsym  6799  ecopovsymg  6802  xpf1o  7029  nneneq  7042  supmoti  7191  supsnti  7203  isotilem  7204  isoti  7205  ltanqg  7619  ltmnqg  7620  elinp  7693  prnmaxl  7707  prnminu  7708  ltasrg  7989  axpre-ltadd  8105  zextle  9570  zextlt  9571  xlesubadd  10117  rexfiuz  11549  climshft  11864  dvdsext  12415  ltoddhalfle  12453  halfleoddlt  12454  bezoutlemmo  12576  bezoutlemeu  12577  bezoutlemle  12578  bezoutlemsup  12579  dfgcd3  12580  dvdssq  12601  rpexp  12724  pcdvdsb  12892  isnsg  13788  nsgbi  13790  elnmz  13794  nmzbi  13795  nmznsg  13799  islidlm  14492  xmeteq0  15082  comet  15222  dedekindeulemuub  15340  dedekindeulemloc  15342  dedekindicclemuub  15349  dedekindicclemloc  15351  logltb  15597  bj-nalset  16490  bj-d0clsepcl  16520  bj-nn0sucALT  16573  ltlenmkv  16674