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  640  xorbi12d  1525  norass  1537  ru0  2128  sbbib  2359  sb8eulem  2591  abbib  2798  cleqh  2857  cleqf  2920  vtoclbg  3514  vtoclb  3525  ceqsexg  3610  elabgf  3632  reu6  3688  ruOLD  3743  sbcbig  3796  unineq  4241  sbcnestgfw  4374  sbcnestgf  4379  preq12bg  4807  axrep1  5222  axrep4OLD  5228  nalset  5255  opthg  5424  opelopabsb  5477  isso2i  5568  opeliunxp2  5785  resieq  5945  dfpo2  6248  cbviotaw  6449  cbviota  6451  iota2df  6473  fnbrfvb  6877  fvelimab  6899  fvopab5  6967  fmptco  7067  fsng  7075  fressnfv  7098  fnpr2g  7150  isorel  7267  isocnv  7271  isocnv3  7273  isotr  7277  eqfunresadj  7301  ovg  7518  caovcang  7554  caovordg  7560  caovord3d  7563  caovord  7564  caofidlcan  7655  orduninsuc  7783  xpord2pred  8085  xpord3pred  8092  opeliunxp2f  8150  brtpos  8175  dftpos4  8185  omopth  8587  ecopovsym  8753  xpf1o  9063  nneneq  9130  ttrclselem2  9641  r1pwALT  9761  karden  9810  infxpenlem  9926  aceq0  10031  cflim2  10176  zfac  10373  ttukeylem1  10422  axextnd  10504  axrepndlem1  10505  axrepndlem2  10506  axrepnd  10507  axacndlem5  10524  zfcndrep  10527  zfcndac  10532  winalim  10608  gruina  10731  ltrnq  10892  ltsosr  11007  ltasr  11013  axpre-lttri  11078  axpre-ltadd  11080  nn0sub  12452  zextle  12567  zextlt  12568  xlesubadd  13183  sqeqor  14141  nn0opth2  14197  rexfiuz  15273  climshft  15501  rpnnen2lem10  16150  dvdsext  16250  ltoddhalfle  16290  halfleoddlt  16291  sumodd  16317  sadcadd  16387  dvdssq  16496  rpexp  16651  pcdvdsb  16799  imasleval  17463  isacs2  17577  acsfiel  17578  funcres2b  17822  pospropd  18249  isnsg  19052  nsgbi  19054  elnmz  19060  nmzbi  19061  oddvdsnn0  19441  odeq  19447  odmulg  19453  isslw  19505  slwispgp  19508  gsumval3lem2  19803  gsumcom2  19872  abveq0  20721  cnt0  23249  kqfvima  23633  kqt0lem  23639  isr0  23640  r0cld  23641  regr1lem2  23643  nrmr0reg  23652  isfildlem  23760  cnextfvval  23968  xmeteq0  24242  imasf1oxmet  24279  comet  24417  dscmet  24476  nrmmetd  24478  tngngp  24558  tngngp3  24560  mbfsup  25581  mbfinf  25582  degltlem1  25993  logltb  26525  cxple2  26622  rlimcnp  26891  rlimcnp2  26892  isppw2  27041  sqf11  27065  slerec  27748  tgjustc1  28438  tgjustc2  28439  f1otrgitv  28833  nbuhgr2vtx1edgb  29315  dfconngr1  30150  eupth2lem3lem6  30195  nmlno0i  30756  nmlno0  30757  blocn  30769  ubth  30835  hvsubeq0  31030  hvaddcan  31032  hvsubadd  31039  normsub0  31098  hlim2  31154  pjoc1  31396  pjoc2  31401  chne0  31456  chsscon3  31462  chlejb1  31474  chnle  31476  h1de2ci  31518  elspansn  31528  elspansn2  31529  cmbr3  31570  cmcm  31576  cmcm3  31577  pjch1  31632  pjch  31656  pj11  31676  pjnel  31688  eigorth  31800  elnlfn  31890  nmlnop0  31960  lnopeq  31971  lnopcon  31997  lnfncon  32018  pjdifnormi  32129  chrelat2  32332  cvexch  32336  mdsym  32374  eqelbid  32437  fmptcof2  32614  mgcoval  32941  mgcval  32942  mgccole1  32945  mgccole2  32946  mgcmnt1  32947  mgcmnt2  32948  mgccnv  32954  unitprodclb  33336  ist0cld  33799  zarclssn  33839  zart0  33845  signswch  34528  fnrelpredd  35055  cvmlift2lem12  35286  cvmlift2lem13  35287  satfv1lem  35334  satf0op  35349  fmlafvel  35357  abs2sqle  35652  abs2sqlt  35653  axextdist  35772  brimageg  35900  brdomaing  35908  brrangeg  35909  elhf2  36148  nn0prpwlem  36295  nn0prpw  36296  onsuct0  36414  bj-sbceqgALT  36875  bj-elabd2ALT  36898  eleq2w2ALT  37020  dfgcd3  37297  cbveud  37345  wl-3xorbi123d  37448  matunitlindf  37597  prdsbnd2  37774  isdrngo1  37935  eqrelf  38229  elsymrels5  38532  dfdisjs5  38689  eldisjs5  38703  mpets2  38818  pets  38829  lsatcmp  38981  llnexchb2  39848  lautset  40061  lautle  40063  sticksstones2  42120  aks6d1c7  42157  dvdsexpnn0  42307  eu6w  42649  abbibw  42650  zindbi  42919  wepwsolem  43015  aomclem8  43034  onsupmaxb  43212  oaordnr  43269  omnord1  43278  oenord1  43289  ntrneik13  44071  ntrneix13  44072  ntrneik4w  44073  2sbc6g  44388  2sbc5g  44389  modelaxreplem3  44954  wessf1ornlem  45163  fourierdlem31  46120  fourierdlem42  46131  fourierdlem54  46142  funressndmafv2rn  47208  dfatbrafv2b  47230  fnbrafv2b  47233  ichbidv  47438  ichnfim  47449  sprsymrelf  47480  sprsymrelfo  47482  isuspgrimlem  47880  line2ylem  48737  line2xlem  48739  mofeu  48833  tposres0  48862  catprslem  48996