Theorem bibi12d 335

Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-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 333	. 2 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	bibi2d 332	. 2 |- ( ph -> ( ( ch <-> th ) <-> ( ch <-> ta ) ) )
5	2, 4	bitrd 268	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  bi2bian9  919  xorbi12d  1478  sb8eu  2503  cleqh  2724  vtoclb  3263  vtoclbg  3267  ceqsexg  3334  elabgf  3348  reu6  3395  ru  3434  sbcbig  3480  unineq  3877  sbcnestgf  3995  preq12bg  4386  prel12g  4387  axrep1  4772  axrep4  4775  nalset  4795  opthg  4946  opelopabsb  4985  isso2i  5067  opeliunxp2  5260  resieq  5407  elimasng  5491  cbviota  5856  iota2df  5875  fnbrfvb  6236  fvelimab  6253  fvopab5  6309  fmptco  6396  fsng  6404  fsn2g  6405  fressnfv  6427  fnpr2g  6474  isorel  6576  isocnv  6580  isocnv3  6582  isotr  6586  ovg  6799  caovcang  6835  caovordg  6841  caovord3d  6844  caovord  6845  orduninsuc  7043  opeliunxp2f  7336  brtpos  7361  dftpos4  7371  omopth  7738  ecopovsym  7849  xpf1o  8122  nneneq  8143  r1pwALT  8709  karden  8758  infxpenlem  8836  aceq0  8941  cflim2  9085  zfac  9282  ttukeylem1  9331  axextnd  9413  axrepndlem1  9414  axrepndlem2  9415  axrepnd  9416  axacndlem5  9433  zfcndrep  9436  zfcndac  9441  winalim  9517  gruina  9640  ltrnq  9801  ltsosr  9915  ltasr  9921  axpre-lttri  9986  axpre-ltadd  9988  nn0sub  11343  zextle  11450  zextlt  11451  xlesubadd  12093  sqeqor  12978  nn0opth2  13059  rexfiuz  14087  climshft  14307  rpnnen2lem10  14952  dvdsext  15043  ltoddhalfle  15085  halfleoddlt  15086  sumodd  15111  sadcadd  15180  dvdssq  15280  rpexp  15432  pcdvdsb  15573  imasleval  16201  isacs2  16314  acsfiel  16315  funcres2b  16557  pospropd  17134  isnsg  17623  nsgbi  17625  elnmz  17633  nmzbi  17634  oddvdsnn0  17963  odeq  17969  odmulg  17973  isslw  18023  slwispgp  18026  gsumval3lem2  18307  gsumcom2  18374  abveq0  18826  cnt0  21150  kqfvima  21533  kqt0lem  21539  isr0  21540  r0cld  21541  regr1lem2  21543  nrmr0reg  21552  isfildlem  21661  cnextfvval  21869  xmeteq0  22143  imasf1oxmet  22180  comet  22318  dscmet  22377  nrmmetd  22379  tngngp  22458  tngngp3  22460  mbfsup  23431  mbfinf  23432  degltlem1  23832  logltb  24346  cxple2  24443  rlimcnp  24692  rlimcnp2  24693  isppw2  24841  sqf11  24865  f1otrgitv  25750  nbuhgr2vtx1edgb  26248  dfconngr1  27048  eupth2lem3lem6  27093  nmlno0i  27649  nmlno0  27650  blocn  27662  ubth  27729  hvsubeq0  27925  hvaddcan  27927  hvsubadd  27934  normsub0  27993  hlim2  28049  pjoc1  28293  pjoc2  28298  chne0  28353  chsscon3  28359  chlejb1  28371  chnle  28373  h1de2ci  28415  elspansn  28425  elspansn2  28426  cmbr3  28467  cmcm  28473  cmcm3  28474  pjch1  28529  pjch  28553  pj11  28573  pjnel  28585  eigorth  28697  elnlfn  28787  nmlnop0  28857  lnopeq  28868  lnopcon  28894  lnfncon  28915  pjdifnormi  29026  chrelat2  29229  cvexch  29233  mdsym  29271  fmptcof2  29457  signswch  30638  cvmlift2lem12  31296  cvmlift2lem13  31297  abs2sqle  31574  abs2sqlt  31575  dfpo2  31645  eqfunresadj  31659  br1steqgOLD  31674  br2ndeqgOLD  31675  axextdist  31705  slerec  31923  brimageg  32034  brdomaing  32042  brrangeg  32043  elhf2  32282  nn0prpwlem  32317  nn0prpw  32318  onsuct0  32440  bj-abbi  32775  bj-axrep1  32788  bj-axrep4  32791  bj-nalset  32794  bj-sbceqgALT  32897  bj-ru0  32932  dfgcd3  33170  matunitlindf  33407  prdsbnd2  33594  isdrngo1  33755  eqrelf  34020  lsatcmp  34290  llnexchb2  35155  lautset  35368  lautle  35370  zindbi  37511  wepwsolem  37612  aomclem8  37631  ntrneik13  38396  ntrneix13  38397  ntrneik4w  38398  2sbc6g  38616  2sbc5g  38617  wessf1ornlem  39371  fourierdlem31  40355  fourierdlem42  40366  fourierdlem54  40377  sprsymrelf  41745  sprsymrelfo  41747