Theorem bibi12d 348

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 346	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 345	. 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
5	2, 4	bitrd 281	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bi2bian9  639  xorbi12d  1517  norass  1532  sbbib  2379  sb8eulem  2683  abbi  2891  cleqh  2939  cleqf  3013  vtoclb  3567  vtoclbg  3572  ceqsexg  3649  elabgf  3667  elabg  3669  reu6  3720  ru  3774  sbcbig  3826  unineq  4257  sbcnestgfw  4373  sbcnestgf  4378  preq12bg  4787  axrep1  5194  axrep4  5198  nalset  5220  opthg  5372  opelopabsb  5420  isso2i  5511  opeliunxp2  5712  resieq  5867  elimasng  5958  cbviotaw  6324  cbviota  6326  iota2df  6345  fnbrfvb  6721  fvelimab  6740  fvopab5  6803  fmptco  6894  fsng  6902  fressnfv  6925  fnpr2g  6976  isorel  7082  isocnv  7086  isocnv3  7088  isotr  7092  ovg  7316  caovcang  7352  caovordg  7358  caovord3d  7361  caovord  7362  orduninsuc  7561  opeliunxp2f  7879  brtpos  7904  dftpos4  7914  omopth  8288  ecopovsym  8402  xpf1o  8682  nneneq  8703  r1pwALT  9278  karden  9327  infxpenlem  9442  aceq0  9547  cflim2  9688  zfac  9885  ttukeylem1  9934  axextnd  10016  axrepndlem1  10017  axrepndlem2  10018  axrepnd  10019  axacndlem5  10036  zfcndrep  10039  zfcndac  10044  winalim  10120  gruina  10243  ltrnq  10404  ltsosr  10519  ltasr  10525  axpre-lttri  10590  axpre-ltadd  10592  nn0sub  11950  zextle  12058  zextlt  12059  xlesubadd  12659  sqeqor  13581  nn0opth2  13635  rexfiuz  14710  climshft  14936  rpnnen2lem10  15579  dvdsext  15674  ltoddhalfle  15713  halfleoddlt  15714  sumodd  15742  sadcadd  15810  dvdssq  15914  rpexp  16067  pcdvdsb  16208  imasleval  16817  isacs2  16927  acsfiel  16928  funcres2b  17170  pospropd  17747  isnsg  18310  nsgbi  18312  elnmz  18318  nmzbi  18319  oddvdsnn0  18675  odeq  18681  odmulg  18686  isslw  18736  slwispgp  18739  gsumval3lem2  19029  gsumcom2  19098  abveq0  19600  cnt0  21957  kqfvima  22341  kqt0lem  22347  isr0  22348  r0cld  22349  regr1lem2  22351  nrmr0reg  22360  isfildlem  22468  cnextfvval  22676  xmeteq0  22951  imasf1oxmet  22988  comet  23126  dscmet  23185  nrmmetd  23187  tngngp  23266  tngngp3  23268  mbfsup  24268  mbfinf  24269  degltlem1  24669  logltb  25186  cxple2  25283  rlimcnp  25546  rlimcnp2  25547  isppw2  25695  sqf11  25719  tgjustc1  26264  tgjustc2  26265  f1otrgitv  26659  nbuhgr2vtx1edgb  27137  dfconngr1  27970  eupth2lem3lem6  28015  nmlno0i  28574  nmlno0  28575  blocn  28587  ubth  28653  hvsubeq0  28848  hvaddcan  28850  hvsubadd  28857  normsub0  28916  hlim2  28972  pjoc1  29214  pjoc2  29219  chne0  29274  chsscon3  29280  chlejb1  29292  chnle  29294  h1de2ci  29336  elspansn  29346  elspansn2  29347  cmbr3  29388  cmcm  29394  cmcm3  29395  pjch1  29450  pjch  29474  pj11  29494  pjnel  29506  eigorth  29618  elnlfn  29708  nmlnop0  29778  lnopeq  29789  lnopcon  29815  lnfncon  29836  pjdifnormi  29947  chrelat2  30150  cvexch  30154  mdsym  30192  fmptcof2  30405  signswch  31835  cvmlift2lem12  32565  cvmlift2lem13  32566  satfv1lem  32613  satf0op  32628  fmlafvel  32636  abs2sqle  32927  abs2sqlt  32928  dfpo2  32995  eqfunresadj  33008  axextdist  33048  slerec  33281  brimageg  33392  brdomaing  33400  brrangeg  33401  elhf2  33640  nn0prpwlem  33674  nn0prpw  33675  onsuct0  33793  bj-sbceqgALT  34223  bj-ru0  34257  dfgcd3  34609  cbveud  34657  matunitlindf  34894  prdsbnd2  35077  isdrngo1  35238  eqrelf  35521  elsymrels5  35796  dfdisjs5  35949  eldisjs5  35963  lsatcmp  36143  llnexchb2  37009  lautset  37222  lautle  37224  sn-elabg  39110  zindbi  39549  wepwsolem  39648  aomclem8  39667  ntrneik13  40454  ntrneix13  40455  ntrneik4w  40456  2sbc6g  40753  2sbc5g  40754  wessf1ornlem  41451  fourierdlem31  42430  fourierdlem42  42441  fourierdlem54  42452  funressndmafv2rn  43429  dfatbrafv2b  43451  fnbrafv2b  43454  ichnfim  43631  sprsymrelf  43664  sprsymrelfo  43666  isomuspgrlem2b  44001  isomuspgrlem2d  44003  line2ylem  44745  line2xlem  44747