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  9615  zextlt  9616  xlesubadd  10162  rexfiuz  11612  climshft  11927  dvdsext  12479  ltoddhalfle  12517  halfleoddlt  12518  bezoutlemmo  12640  bezoutlemeu  12641  bezoutlemle  12642  bezoutlemsup  12643  dfgcd3  12644  dvdssq  12665  rpexp  12788  pcdvdsb  12956  isnsg  13852  nsgbi  13854  elnmz  13858  nmzbi  13859  nmznsg  13863  islidlm  14558  xmeteq0  15153  comet  15293  dedekindeulemuub  15411  dedekindeulemloc  15413  dedekindicclemuub  15420  dedekindicclemloc  15422  logltb  15668  eupth2lem3lem6fi  16395  bj-nalset  16594  bj-d0clsepcl  16624  bj-nn0sucALT  16677  ltlenmkv  16786