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  abbib  2349  cleqf  2400  cbvreuvw  2774  vtoclb  2862  vtoclbg  2866  ceqsexg  2935  elabgf  2949  reu6  2996  ru  3031  sbcbig  3079  sbcne12g  3146  sbcnestgf  3180  preq12bg  3861  nalset  4224  undifexmid  4289  exmidsssn  4298  exmidsssnc  4299  exmidundif  4302  opthg  4336  opelopabsb  4360  wetriext  4681  opeliunxp2  4876  resieq  5029  elimasng  5111  cbviota  5298  iota2df  5319  fnbrfvb  5693  fvelimab  5711  fmptco  5821  fsng  5828  fressnfv  5849  funfvima3  5898  isorel  5959  isocnv  5962  isocnv2  5963  isotr  5967  ovg  6171  caovcang  6194  caovordg  6200  caovord3d  6203  caovord  6204  uchoice  6309  opeliunxp2f  6447  dftpos4  6472  ecopovsym  6843  ecopovsymg  6846  xpf1o  7073  nneneq  7086  supmoti  7235  supsnti  7247  isotilem  7248  isoti  7249  ltanqg  7663  ltmnqg  7664  elinp  7737  prnmaxl  7751  prnminu  7752  ltasrg  8033  axpre-ltadd  8149  zextle  9614  zextlt  9615  xlesubadd  10161  rexfiuz  11610  climshft  11925  dvdsext  12477  ltoddhalfle  12515  halfleoddlt  12516  bezoutlemmo  12638  bezoutlemeu  12639  bezoutlemle  12640  bezoutlemsup  12641  dfgcd3  12642  dvdssq  12663  rpexp  12786  pcdvdsb  12954  isnsg  13850  nsgbi  13852  elnmz  13856  nmzbi  13857  nmznsg  13861  islidlm  14555  xmeteq0  15150  comet  15290  dedekindeulemuub  15408  dedekindeulemloc  15410  dedekindicclemuub  15417  dedekindicclemloc  15419  logltb  15665  eupth2lem3lem6fi  16389  bj-nalset  16588  bj-d0clsepcl  16618  bj-nn0sucALT  16671  ltlenmkv  16780