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 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bi2bian9  652  xorbi12d  1555  norass  1567  ru0  2164  sbbib  2392  sb8eulem  2625  abbib  2831  cleqh  2891  cleqf  2952  vtoclbg  3522  vtoclb  3531  ceqsexg  3610  elabgf  3631  reu6  3687  sbcbig  3793  unineq  4237  sbcnestgfw  4382  sbcnestgf  4387  preq12bg  4816  axrep1  5237  axrep4OLD  5243  nalsetOLD  5276  opthg  5457  opelopabsb  5512  isso2i  5604  opeliunxp2  5822  resieq  5987  dfpo2  6298  cbviotaw  6500  cbviota  6502  iota2df  6524  fnbrfvb  6932  fvelimab  6954  fvopab5  7024  fmptco  7127  fsng  7135  fressnfv  7161  fnpr2g  7213  isorel  7331  isocnv  7335  isocnv3  7337  isotr  7341  eqfunresadj  7367  ovg  7582  caovcang  7619  caovordg  7625  caovord3d  7628  caovord  7629  caofidlcan  7720  orduninsuc  7843  xpord2pred  8147  xpord3pred  8154  opeliunxp2f  8212  brtpos  8237  dftpos4  8247  omopth  8654  ecopovsym  8823  xpf1o  9141  nneneq  9204  ttrclselem2  9709  r1pwALT  9832  kardenOLD  9903  infxpenlem  10020  aceq0  10125  cflim2  10269  zfac  10466  ttukeylem1  10515  axextnd  10604  axrepndlem1  10605  axrepndlem2  10606  axrepnd  10607  axacndlem5  10624  zfcndrep  10627  zfcndac  10632  winalim  10708  gruina  10831  ltrnq  10992  ltsosr  11107  ltasr  11113  axpre-lttri  11178  axpre-ltadd  11180  nn0sub  12582  zextle  12698  zextlt  12699  xlesubadd  13319  sqeqor  14284  nn0opth2  14340  rexfiuz  15439  climshft  15667  rpnnen2lem10  16317  dvdsext  16417  ltoddhalfle  16457  halfleoddlt  16458  sumodd  16484  sadcadd  16554  dvdssq  16663  rpexp  16819  pcdvdsb  16967  imasleval  17633  isacs2  17747  acsfiel  17748  funcres2b  17992  pospropd  18419  isnsg  19284  nsgbi  19286  elnmz  19292  nmzbi  19293  oddvdsnn0  19677  odeq  19683  odmulg  19689  isslw  19741  slwispgp  19744  gsumval3lem2  20039  gsumcom2  20108  abveq0  20990  matunitlindf  22909  cnt0  23577  kqfvima  23962  kqt0lem  23968  isr0  23969  r0cld  23970  regr1lem2  23972  nrmr0reg  23981  isfildlem  24089  cnextfvval  24297  xmeteq0  24570  imasf1oxmet  24607  comet  24745  dscmet  24804  nrmmetd  24806  tngngp  24886  tngngp3  24888  mbfsup  25898  mbfinf  25899  degltlem1  26304  logltb  26845  cxple2  26942  rlimcnp  27210  rlimcnp2  27211  isppw2  27359  sqf11  27383  lesrec  28072  tgjustc1  28824  tgjustc2  28825  f1otrgitv  29334  nbuhgr2vtx1edgb  29820  dfconngr1  30676  eupth2lem3lem6  30721  nmlno0i  31283  nmlno0  31284  blocn  31296  ubth  31362  hvsubeq0  31557  hvaddcan  31559  hvsubadd  31566  normsub0  31625  hlim2  31681  pjoc1  31923  pjoc2  31928  chne0  31983  chsscon3  31989  chlejb1  32001  chnle  32003  h1de2ci  32045  elspansn  32055  elspansn2  32056  cmbr3  32097  cmcm  32103  cmcm3  32104  pjch1  32159  pjch  32183  pj11  32203  pjnel  32215  eigorth  32327  elnlfn  32417  nmlnop0  32487  lnopeq  32498  lnopcon  32524  lnfncon  32545  pjdifnormi  32656  chrelat2  32859  cvexch  32863  mdsym  32901  eqelbid  32958  fmptcof2  33138  mgcoval  33434  mgcval  33435  mgccole1  33438  mgccole2  33439  mgcmnt1  33440  mgcmnt2  33441  mgccnv  33447  domnprodeq0  33727  unitprodclb  33830  ist0cld  34351  zarclssn  34391  zart0  34397  signswch  35077  fnrelpredd  35604  r1omhfb  35630  r1omhfbregs  35671  axsepg2  35674  axsepg4  35677  cvmlift2lem12  35901  cvmlift2lem13  35902  satfv1lem  35949  satf0op  35964  fmlafvel  35972  abs2sqle  36267  abs2sqlt  36268  axextdist  36384  brimageg  36512  brdomaing  36520  brrangeg  36521  elhf2  36763  nn0prpwlem  36949  nn0prpw  36950  onsuct0  37068  ttcwf2  37152  bj-sbceqgALT  37653  bj-elabd2ALT  37677  eleq2w2ALT  37799  bj-axseprep  37827  dfgcd3  38084  cbveud  38134  wl-3xorbi123d  38237  wl-dfcleq  38276  prdsbnd2  38553  isdrngo1  38714  eqrelf  39014  elsymrels5  39396  dfdisjs5  39553  eldisjs5  39579  mpets2  39711  pets  39722  lsatcmp  39884  llnexchb2  40750  lautset  40963  lautle  40965  sticksstones2  43021  aks6d1c7  43058  dvdsexpnn0  43217  eu6w  43530  abbibw  43531  zindbi  43795  wepwsolem  43891  aomclem8  43910  onsupmaxb  44088  oaordnr  44145  omnord1  44154  oenord1  44165  ntrneik13  44946  ntrneix13  44947  ntrneik4w  44948  2sbc6g  45247  2sbc5g  45248  modelaxreplem3  45811  wessf1ornlem  46025  fourierdlem31  46974  fourierdlem42  46985  fourierdlem54  46996  funressndmafv2rn  48119  dfatbrafv2b  48141  fnbrafv2b  48144  ichbidv  48361  ichnfim  48372  sprsymrelf  48403  sprsymrelfo  48405  isuspgrimlem  48819  line2ylem  49689  line2xlem  49691  mofeu  49784  tposres0  49811  catprslem  49944