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 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  651  xorbi12d  1555  norass  1567  ru0  2162  sbbib  2393  sb8eulem  2626  abbib  2832  cleqh  2892  cleqf  2953  vtoclbg  3525  vtoclb  3534  ceqsexg  3613  elabgf  3634  reu6  3690  sbcbig  3796  unineq  4242  sbcnestgfw  4387  sbcnestgf  4392  preq12bg  4819  axrep1  5240  axrep4OLD  5246  nalsetOLD  5279  opthg  5461  opelopabsb  5516  isso2i  5608  opeliunxp2  5826  resieq  5991  dfpo2  6299  cbviotaw  6501  cbviota  6503  iota2df  6525  fnbrfvb  6933  fvelimab  6955  fvopab5  7025  fmptco  7127  fsng  7135  fressnfv  7159  fnpr2g  7210  isorel  7326  isocnv  7330  isocnv3  7332  isotr  7336  eqfunresadj  7360  ovg  7577  caovcang  7613  caovordg  7619  caovord3d  7622  caovord  7623  caofidlcan  7714  orduninsuc  7840  xpord2pred  8142  xpord3pred  8149  opeliunxp2f  8207  brtpos  8232  dftpos4  8242  omopth  8649  ecopovsym  8818  xpf1o  9128  nneneq  9191  ttrclselem2  9696  r1pwALT  9819  karden  9882  infxpenlem  9998  aceq0  10103  cflim2  10248  zfac  10445  ttukeylem1  10494  axextnd  10577  axrepndlem1  10578  axrepndlem2  10579  axrepnd  10580  axacndlem5  10597  zfcndrep  10600  zfcndac  10605  winalim  10681  gruina  10804  ltrnq  10965  ltsosr  11080  ltasr  11086  axpre-lttri  11151  axpre-ltadd  11153  nn0sub  12555  zextle  12670  zextlt  12671  xlesubadd  13290  sqeqor  14254  nn0opth2  14310  rexfiuz  15401  climshft  15629  rpnnen2lem10  16280  dvdsext  16380  ltoddhalfle  16420  halfleoddlt  16421  sumodd  16447  sadcadd  16517  dvdssq  16626  rpexp  16782  pcdvdsb  16930  imasleval  17596  isacs2  17710  acsfiel  17711  funcres2b  17955  pospropd  18382  isnsg  19222  nsgbi  19224  elnmz  19230  nmzbi  19231  oddvdsnn0  19615  odeq  19621  odmulg  19627  isslw  19679  slwispgp  19682  gsumval3lem2  19977  gsumcom2  20046  abveq0  20902  cnt0  23484  kqfvima  23868  kqt0lem  23874  isr0  23875  r0cld  23876  regr1lem2  23878  nrmr0reg  23887  isfildlem  23995  cnextfvval  24203  xmeteq0  24476  imasf1oxmet  24513  comet  24651  dscmet  24710  nrmmetd  24712  tngngp  24792  tngngp3  24794  mbfsup  25804  mbfinf  25805  degltlem1  26210  logltb  26746  cxple2  26843  rlimcnp  27111  rlimcnp2  27112  isppw2  27260  sqf11  27284  lesrec  27973  tgjustc1  28725  tgjustc2  28726  f1otrgitv  29200  nbuhgr2vtx1edgb  29683  dfconngr1  30520  eupth2lem3lem6  30565  nmlno0i  31127  nmlno0  31128  blocn  31140  ubth  31206  hvsubeq0  31401  hvaddcan  31403  hvsubadd  31410  normsub0  31469  hlim2  31525  pjoc1  31767  pjoc2  31772  chne0  31827  chsscon3  31833  chlejb1  31845  chnle  31847  h1de2ci  31889  elspansn  31899  elspansn2  31900  cmbr3  31941  cmcm  31947  cmcm3  31948  pjch1  32003  pjch  32027  pj11  32047  pjnel  32059  eigorth  32171  elnlfn  32261  nmlnop0  32331  lnopeq  32342  lnopcon  32368  lnfncon  32389  pjdifnormi  32500  chrelat2  32703  cvexch  32707  mdsym  32745  eqelbid  32802  fmptcof2  32983  mgcoval  33287  mgcval  33288  mgccole1  33291  mgccole2  33292  mgcmnt1  33293  mgcmnt2  33294  mgccnv  33300  domnprodeq0  33580  unitprodclb  33683  ist0cld  34204  zarclssn  34244  zart0  34250  signswch  34929  fnrelpredd  35463  r1omhfb  35489  r1omhfbregs  35531  axsepg2  35534  axsepg4  35537  cvmlift2lem12  35787  cvmlift2lem13  35788  satfv1lem  35835  satf0op  35850  fmlafvel  35858  abs2sqle  36153  abs2sqlt  36154  axextdist  36270  brimageg  36398  brdomaing  36406  brrangeg  36407  elhf2  36648  nn0prpwlem  36814  nn0prpw  36815  onsuct0  36933  ttcwf2  37017  bj-sbceqgALT  37518  bj-elabd2ALT  37542  eleq2w2ALT  37664  bj-axseprep  37692  dfgcd3  37949  cbveud  37999  wl-3xorbi123d  38102  wl-dfcleq  38141  matunitlindf  38250  prdsbnd2  38427  isdrngo1  38588  eqrelf  38888  elsymrels5  39270  dfdisjs5  39427  eldisjs5  39453  mpets2  39585  pets  39596  lsatcmp  39758  llnexchb2  40624  lautset  40837  lautle  40839  sticksstones2  42895  aks6d1c7  42932  dvdsexpnn0  43076  eu6w  43391  abbibw  43392  zindbi  43656  wepwsolem  43752  aomclem8  43771  onsupmaxb  43949  oaordnr  44006  omnord1  44015  oenord1  44026  ntrneik13  44807  ntrneix13  44808  ntrneik4w  44809  2sbc6g  45108  2sbc5g  45109  modelaxreplem3  45672  wessf1ornlem  45886  fourierdlem31  46835  fourierdlem42  46846  fourierdlem54  46857  funressndmafv2rn  47943  dfatbrafv2b  47965  fnbrafv2b  47968  ichbidv  48185  ichnfim  48196  sprsymrelf  48227  sprsymrelfo  48229  isuspgrimlem  48643  line2ylem  49514  line2xlem  49516  mofeu  49609  tposres0  49638  catprslem  49771