Theorem bibi12d 345

Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-1993.)

Hypotheses

Ref	Expression
imbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
imbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
bibi12d	⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Proof of Theorem bibi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	bibi1d 343	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 342	. 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
5	2, 4	bitrd 279	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bi2bian9  641  xorbi12d  1527  norass  1539  ru0  2133  sbbib  2365  sb8eulem  2598  abbib  2805  cleqh  2865  cleqf  2927  vtoclbg  3502  vtoclb  3512  ceqsexg  3595  elabgf  3617  reu6  3672  ruOLD  3727  sbcbig  3780  unineq  4228  sbcnestgfw  4361  sbcnestgf  4366  preq12bg  4796  axrep1  5213  axrep4OLD  5219  nalsetOLD  5250  opthg  5430  opelopabsb  5485  isso2i  5576  opeliunxp2  5793  resieq  5955  dfpo2  6260  cbviotaw  6461  cbviota  6463  iota2df  6485  fnbrfvb  6890  fvelimab  6912  fvopab5  6981  fmptco  7082  fsng  7090  fressnfv  7114  fnpr2g  7165  isorel  7281  isocnv  7285  isocnv3  7287  isotr  7291  eqfunresadj  7315  ovg  7532  caovcang  7568  caovordg  7574  caovord3d  7577  caovord  7578  caofidlcan  7669  orduninsuc  7794  xpord2pred  8095  xpord3pred  8102  opeliunxp2f  8160  brtpos  8185  dftpos4  8195  omopth  8598  ecopovsym  8766  xpf1o  9077  nneneq  9140  ttrclselem2  9647  r1pwALT  9770  karden  9819  infxpenlem  9935  aceq0  10040  cflim2  10185  zfac  10382  ttukeylem1  10431  axextnd  10514  axrepndlem1  10515  axrepndlem2  10516  axrepnd  10517  axacndlem5  10534  zfcndrep  10537  zfcndac  10542  winalim  10618  gruina  10741  ltrnq  10902  ltsosr  11017  ltasr  11023  axpre-lttri  11088  axpre-ltadd  11090  nn0sub  12487  zextle  12602  zextlt  12603  xlesubadd  13215  sqeqor  14178  nn0opth2  14234  rexfiuz  15310  climshft  15538  rpnnen2lem10  16190  dvdsext  16290  ltoddhalfle  16330  halfleoddlt  16331  sumodd  16357  sadcadd  16427  dvdssq  16536  rpexp  16692  pcdvdsb  16840  imasleval  17505  isacs2  17619  acsfiel  17620  funcres2b  17864  pospropd  18291  isnsg  19130  nsgbi  19132  elnmz  19138  nmzbi  19139  oddvdsnn0  19519  odeq  19525  odmulg  19531  isslw  19583  slwispgp  19586  gsumval3lem2  19881  gsumcom2  19950  abveq0  20795  cnt0  23311  kqfvima  23695  kqt0lem  23701  isr0  23702  r0cld  23703  regr1lem2  23705  nrmr0reg  23714  isfildlem  23822  cnextfvval  24030  xmeteq0  24303  imasf1oxmet  24340  comet  24478  dscmet  24537  nrmmetd  24539  tngngp  24619  tngngp3  24621  mbfsup  25631  mbfinf  25632  degltlem1  26037  logltb  26564  cxple2  26661  rlimcnp  26929  rlimcnp2  26930  isppw2  27078  sqf11  27102  lesrec  27791  tgjustc1  28543  tgjustc2  28544  f1otrgitv  28938  nbuhgr2vtx1edgb  29421  dfconngr1  30258  eupth2lem3lem6  30303  nmlno0i  30865  nmlno0  30866  blocn  30878  ubth  30944  hvsubeq0  31139  hvaddcan  31141  hvsubadd  31148  normsub0  31207  hlim2  31263  pjoc1  31505  pjoc2  31510  chne0  31565  chsscon3  31571  chlejb1  31583  chnle  31585  h1de2ci  31627  elspansn  31637  elspansn2  31638  cmbr3  31679  cmcm  31685  cmcm3  31686  pjch1  31741  pjch  31765  pj11  31785  pjnel  31797  eigorth  31909  elnlfn  31999  nmlnop0  32069  lnopeq  32080  lnopcon  32106  lnfncon  32127  pjdifnormi  32238  chrelat2  32441  cvexch  32445  mdsym  32483  eqelbid  32544  fmptcof2  32730  mgcoval  33046  mgcval  33047  mgccole1  33050  mgccole2  33051  mgcmnt1  33052  mgcmnt2  33053  mgccnv  33059  domnprodeq0  33337  unitprodclb  33449  ist0cld  33977  zarclssn  34017  zart0  34023  signswch  34705  fnrelpredd  35234  r1omhfb  35256  r1omhfbregs  35281  cvmlift2lem12  35496  cvmlift2lem13  35497  satfv1lem  35544  satf0op  35559  fmlafvel  35567  abs2sqle  35862  abs2sqlt  35863  axextdist  35979  brimageg  36107  brdomaing  36115  brrangeg  36116  elhf2  36357  nn0prpwlem  36504  nn0prpw  36505  onsuct0  36623  ttcwf2  36707  bj-sbceqgALT  37209  bj-elabd2ALT  37232  eleq2w2ALT  37354  bj-axseprep  37381  dfgcd3  37638  cbveud  37688  wl-3xorbi123d  37791  wl-dfcleq  37830  matunitlindf  37939  prdsbnd2  38116  isdrngo1  38277  eqrelf  38579  elsymrels5  38961  dfdisjs5  39118  eldisjs5  39144  mpets2  39276  pets  39287  lsatcmp  39449  llnexchb2  40315  lautset  40528  lautle  40530  sticksstones2  42586  aks6d1c7  42623  dvdsexpnn0  42766  eu6w  43109  abbibw  43110  zindbi  43374  wepwsolem  43470  aomclem8  43489  onsupmaxb  43667  oaordnr  43724  omnord1  43733  oenord1  43744  ntrneik13  44525  ntrneix13  44526  ntrneik4w  44527  2sbc6g  44842  2sbc5g  44843  modelaxreplem3  45407  wessf1ornlem  45615  fourierdlem31  46566  fourierdlem42  46577  fourierdlem54  46588  funressndmafv2rn  47671  dfatbrafv2b  47693  fnbrafv2b  47696  ichbidv  47913  ichnfim  47924  sprsymrelf  47955  sprsymrelfo  47957  isuspgrimlem  48371  line2ylem  49227  line2xlem  49229  mofeu  49323  tposres0  49352  catprslem  49485