Theorem bibi12d 321

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 319	. 2 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	bibi2d 318	. 2 |- ( ph -> ( ( ch <-> th ) <-> ( ch <-> ta ) ) )
5	2, 4	bitrd 253	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )

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

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 185

This theorem is referenced by:  bi2bian9  870  xorbi12d  1364  sb8eu  2292  cleqh  2542  cleqhOLD  2543  abbiOLD  2559  cleqfOLD  2616  vtoclb  3048  vtoclbg  3052  ceqsexg  3112  elabgf  3125  reu6  3169  ru  3206  sbcbig  3254  unineq  3621  sbcnestgf  3712  preq12bg  4072  prel12g  4073  axrep1  4425  axrep4  4428  nalset  4450  opthg  4588  opelopabsb  4620  isso2i  4694  opeliunxp2  4999  resieq  5142  elimasng  5216  cbviota  5407  iota2df  5426  fnbrfvb  5753  fvelimab  5768  fvopab5  5816  fmptco  5897  fsng  5903  fressnfv  5917  isorel  6038  isocnv  6042  isocnv3  6044  isotr  6048  ovg  6250  caovcang  6285  caovordg  6291  caovord3d  6294  caovord  6295  orduninsuc  6475  brtpos  6775  dftpos4  6785  omopth  7118  ecopovsym  7223  xpf1o  7494  nneneq  7515  r1pwOLD  8074  karden  8123  infxpenlem  8201  aceq0  8309  cflim2  8453  zfac  8650  ttukeylem1  8699  axextnd  8776  axrepndlem1  8777  axrepndlem2  8778  axrepnd  8779  axacndlem5  8799  zfcndrep  8802  zfcndac  8807  winalim  8883  gruina  9006  ltrnq  9169  ltsosr  9282  ltasr  9288  axpre-lttri  9353  axpre-ltadd  9355  nn0sub  10651  zextle  10736  zextlt  10737  xlesubadd  11247  sqeqor  12001  nn0opth2  12071  rexfiuz  12856  climshft  13075  rpnnen2lem10  13527  dvdsext  13605  sadcadd  13675  dvdssq  13765  isprm2lem  13791  rpexp  13827  pcdvdsb  13956  imasleval  14500  isacs2  14612  acsfiel  14613  funcres2b  14828  pospropd  15325  isnsg  15731  nsgbi  15733  elnmz  15741  nmzbi  15742  oddvdsnn0  16068  odeq  16074  odmulg  16078  isslw  16128  slwispgp  16131  gsumval3OLD  16403  gsumval3lem2  16405  gsumcom2  16489  abveq0  16933  cnt0  18972  kqfvima  19325  kqt0lem  19331  isr0  19332  r0cld  19333  regr1lem2  19335  nrmr0reg  19344  isfildlem  19452  cnextfvval  19659  xmeteq0  19935  imasf1oxmet  19972  comet  20110  dscmet  20187  nrmmetd  20189  tngngp  20262  mbfsup  21164  mbfinf  21165  degltlem1  21565  logltb  22070  cxple2  22164  rlimcnp  22381  rlimcnp2  22382  isppw2  22475  sqf11  22499  f1otrgitv  23138  eupath2lem3  23622  nmlno0i  24216  nmlno0  24217  blocn  24229  ubth  24296  hvsubeq0  24492  hvaddcan  24494  hvsubadd  24501  normsub0  24560  hlim2  24616  pjoc1  24859  pjoc2  24864  chne0  24919  chsscon3  24925  chlejb1  24937  chnle  24939  h1de2ci  24981  elspansn  24991  elspansn2  24992  cmbr3  25033  cmcm  25039  cmcm3  25040  pjch1  25095  pjch  25119  pj11  25139  pjnel  25151  eigorth  25264  elnlfn  25354  nmlnop0  25424  lnopeq  25435  lnopcon  25461  lnfncon  25482  pjdifnormi  25593  chrelat2  25796  cvexch  25800  mdsym  25838  fmptcof2  26001  fcnvgreu  26013  signswch  26984  cvmlift2lem12  27225  cvmlift2lem13  27226  abs2sqle  27347  abs2sqlt  27348  dfpo2  27587  axextdist  27635  brimageg  27980  brdomaing  27988  brrangeg  27989  elhf2  28235  onsuct0  28309  nn0prpwlem  28543  nn0prpw  28544  prdsbnd2  28720  isdrngo1  28788  sbcalf  28946  sbcexf  28947  zindbi  29313  divalgmodcl  29362  wepwsolem  29420  aomclem8  29440  2sbc6g  29695  2sbc5g  29696  bj-cleqh  32389  bj-abbi  32392  bj-axrep1  32405  bj-axrep4  32408  bj-nalset  32411  bj-sbceqgALT  32500  bj-ru0  32531  lsatcmp  32744  llnexchb2  33609  lautset  33822  lautle  33824