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  2332  abbibcom  2346  abbib  2350  cleqf  2409  cbvreuvw  2784  vtoclb  2872  vtoclbg  2876  ceqsexg  2945  elabgf  2959  reu6  3006  ru  3041  sbcbig  3089  sbcne12g  3156  sbcnestgf  3190  preq12bg  3877  nalset  4240  undifexmid  4306  exmidsssn  4315  exmidsssnc  4316  exmidundif  4319  opthg  4354  opelopabsb  4378  wetriext  4699  opeliunxp2  4895  resieq  5048  elimasng  5130  cbviota  5317  iota2df  5338  fnbrfvb  5715  fvelimab  5733  fmptco  5843  fsng  5850  fressnfv  5871  funfvima3  5920  isorel  5981  isocnv  5984  isocnv2  5985  isotr  5989  ovg  6193  caovcang  6216  caovordg  6222  caovord3d  6225  caovord  6226  uchoice  6331  opeliunxp2f  6469  dftpos4  6494  ecopovsym  6865  ecopovsymg  6868  xpf1o  7097  nneneq  7111  supmoti  7284  supsnti  7296  isotilem  7297  isoti  7298  ltanqg  7715  ltmnqg  7716  elinp  7789  prnmaxl  7803  prnminu  7804  ltasrg  8085  axpre-ltadd  8201  zextle  9669  zextlt  9670  xlesubadd  10216  rexfiuz  11674  climshft  11989  dvdsext  12541  ltoddhalfle  12579  halfleoddlt  12580  bezoutlemmo  12702  bezoutlemeu  12703  bezoutlemle  12704  bezoutlemsup  12705  dfgcd3  12706  dvdssq  12727  rpexp  12850  pcdvdsb  13018  isnsg  13919  nsgbi  13921  elnmz  13925  nmzbi  13926  nmznsg  13930  islidlm  14627  xmeteq0  15224  comet  15364  dedekindeulemuub  15482  dedekindeulemloc  15484  dedekindicclemuub  15491  dedekindicclemloc  15493  logltb  15739  eupth2lem3lem6fi  16466  bj-nalset  16665  bj-d0clsepcl  16695  bj-nn0sucALT  16748  ltlenmkv  16856