Theorem bibi12d 349

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bi2bian9  641  xorbi12d  1523  norass  1539  sbbib  2361  sb8eulem  2597  abbi  2803  cleqh  2854  clelab  2873  cleqf  2928  vtoclb  3468  vtoclbg  3473  ceqsexg  3550  elabgf  3572  elabgOLD  3575  reu6  3628  ru  3682  sbcbig  3737  unineq  4178  sbcnestgfw  4319  sbcnestgf  4324  preq12bg  4750  axrep1  5165  axrep4  5169  nalset  5191  opthg  5346  opelopabsb  5396  isso2i  5488  opeliunxp2  5692  resieq  5847  elimasng  5940  cbviotaw  6323  cbviota  6326  iota2df  6345  fnbrfvb  6743  fvelimab  6762  fvopab5  6828  fmptco  6922  fsng  6930  fressnfv  6953  fnpr2g  7004  isorel  7113  isocnv  7117  isocnv3  7119  isotr  7123  ovg  7351  caovcang  7387  caovordg  7393  caovord3d  7396  caovord  7397  orduninsuc  7600  opeliunxp2f  7930  brtpos  7955  dftpos4  7965  omopth  8365  ecopovsym  8479  xpf1o  8786  nneneq  8807  r1pwALT  9427  karden  9476  infxpenlem  9592  aceq0  9697  cflim2  9842  zfac  10039  ttukeylem1  10088  axextnd  10170  axrepndlem1  10171  axrepndlem2  10172  axrepnd  10173  axacndlem5  10190  zfcndrep  10193  zfcndac  10198  winalim  10274  gruina  10397  ltrnq  10558  ltsosr  10673  ltasr  10679  axpre-lttri  10744  axpre-ltadd  10746  nn0sub  12105  zextle  12215  zextlt  12216  xlesubadd  12818  sqeqor  13749  nn0opth2  13803  rexfiuz  14876  climshft  15102  rpnnen2lem10  15747  dvdsext  15845  ltoddhalfle  15885  halfleoddlt  15886  sumodd  15912  sadcadd  15980  dvdssq  16087  rpexp  16242  pcdvdsb  16385  imasleval  17000  isacs2  17110  acsfiel  17111  funcres2b  17357  pospropd  17787  isnsg  18525  nsgbi  18527  elnmz  18533  nmzbi  18534  oddvdsnn0  18890  odeq  18896  odmulg  18901  isslw  18951  slwispgp  18954  gsumval3lem2  19245  gsumcom2  19314  abveq0  19816  cnt0  22197  kqfvima  22581  kqt0lem  22587  isr0  22588  r0cld  22589  regr1lem2  22591  nrmr0reg  22600  isfildlem  22708  cnextfvval  22916  xmeteq0  23190  imasf1oxmet  23227  comet  23365  dscmet  23424  nrmmetd  23426  tngngp  23506  tngngp3  23508  mbfsup  24515  mbfinf  24516  degltlem1  24924  logltb  25442  cxple2  25539  rlimcnp  25802  rlimcnp2  25803  isppw2  25951  sqf11  25975  tgjustc1  26520  tgjustc2  26521  f1otrgitv  26915  nbuhgr2vtx1edgb  27394  dfconngr1  28225  eupth2lem3lem6  28270  nmlno0i  28829  nmlno0  28830  blocn  28842  ubth  28908  hvsubeq0  29103  hvaddcan  29105  hvsubadd  29112  normsub0  29171  hlim2  29227  pjoc1  29469  pjoc2  29474  chne0  29529  chsscon3  29535  chlejb1  29547  chnle  29549  h1de2ci  29591  elspansn  29601  elspansn2  29602  cmbr3  29643  cmcm  29649  cmcm3  29650  pjch1  29705  pjch  29729  pj11  29749  pjnel  29761  eigorth  29873  elnlfn  29963  nmlnop0  30033  lnopeq  30044  lnopcon  30070  lnfncon  30091  pjdifnormi  30202  chrelat2  30405  cvexch  30409  mdsym  30447  fmptcof2  30668  mgcoval  30937  mgcval  30938  mgccole1  30941  mgccole2  30942  mgcmnt1  30943  mgcmnt2  30944  mgccnv  30950  ist0cld  31451  zarclssn  31491  zart0  31497  signswch  32206  fnrelpredd  32728  cvmlift2lem12  32943  cvmlift2lem13  32944  satfv1lem  32991  satf0op  33006  fmlafvel  33014  abs2sqle  33305  abs2sqlt  33306  dfpo2  33392  eqfunresadj  33405  axextdist  33445  xpord2pred  33472  xpord3pred  33478  slerec  33699  brimageg  33915  brdomaing  33923  brrangeg  33924  elhf2  34163  nn0prpwlem  34197  nn0prpw  34198  onsuct0  34316  bj-sbceqgALT  34774  bj-ru0  34817  eleq2w2ALT  34906  dfgcd3  35178  cbveud  35229  wl-3xorbi123d  35332  matunitlindf  35461  prdsbnd2  35639  isdrngo1  35800  eqrelf  36081  elsymrels5  36356  dfdisjs5  36509  eldisjs5  36523  lsatcmp  36703  llnexchb2  37569  lautset  37782  lautle  37784  sticksstones2  39772  dvdsexpnn0  39990  zindbi  40412  wepwsolem  40511  aomclem8  40530  ntrneik13  41326  ntrneix13  41327  ntrneik4w  41328  2sbc6g  41647  2sbc5g  41648  wessf1ornlem  42336  fourierdlem31  43297  fourierdlem42  43308  fourierdlem54  43319  funressndmafv2rn  44330  dfatbrafv2b  44352  fnbrafv2b  44355  ichbidv  44521  ichnfim  44532  sprsymrelf  44563  sprsymrelfo  44565  isomuspgrlem2b  44897  isomuspgrlem2d  44899  line2ylem  45713  line2xlem  45715  mofeu  45791  catprslem  45907