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  2127  sbbib  2364  sb8eulem  2598  abbib  2811  cleqh  2871  cleqf  2934  vtoclbg  3557  vtoclb  3568  ceqsexg  3653  elabgf  3674  reu6  3732  ruOLD  3787  sbcbig  3840  unineq  4288  sbcnestgfw  4421  sbcnestgf  4426  preq12bg  4853  axrep1  5280  axrep4OLD  5286  nalset  5313  opthg  5482  opelopabsb  5535  isso2i  5629  opeliunxp2  5849  resieq  6008  dfpo2  6316  cbviotaw  6521  cbviota  6523  iota2df  6548  fnbrfvb  6959  fvelimab  6981  fvopab5  7049  fmptco  7149  fsng  7157  fressnfv  7180  fnpr2g  7230  isorel  7346  isocnv  7350  isocnv3  7352  isotr  7356  eqfunresadj  7380  ovg  7598  caovcang  7634  caovordg  7640  caovord3d  7643  caovord  7644  caofidlcan  7735  orduninsuc  7864  xpord2pred  8170  xpord3pred  8177  opeliunxp2f  8235  brtpos  8260  dftpos4  8270  omopth  8700  ecopovsym  8859  xpf1o  9179  nneneq  9246  nneneqOLD  9258  ttrclselem2  9766  r1pwALT  9886  karden  9935  infxpenlem  10053  aceq0  10158  cflim2  10303  zfac  10500  ttukeylem1  10549  axextnd  10631  axrepndlem1  10632  axrepndlem2  10633  axrepnd  10634  axacndlem5  10651  zfcndrep  10654  zfcndac  10659  winalim  10735  gruina  10858  ltrnq  11019  ltsosr  11134  ltasr  11140  axpre-lttri  11205  axpre-ltadd  11207  nn0sub  12576  zextle  12691  zextlt  12692  xlesubadd  13305  sqeqor  14255  nn0opth2  14311  rexfiuz  15386  climshft  15612  rpnnen2lem10  16259  dvdsext  16358  ltoddhalfle  16398  halfleoddlt  16399  sumodd  16425  sadcadd  16495  dvdssq  16604  rpexp  16759  pcdvdsb  16907  imasleval  17586  isacs2  17696  acsfiel  17697  funcres2b  17942  pospropd  18372  isnsg  19173  nsgbi  19175  elnmz  19181  nmzbi  19182  oddvdsnn0  19562  odeq  19568  odmulg  19574  isslw  19626  slwispgp  19629  gsumval3lem2  19924  gsumcom2  19993  abveq0  20819  cnt0  23354  kqfvima  23738  kqt0lem  23744  isr0  23745  r0cld  23746  regr1lem2  23748  nrmr0reg  23757  isfildlem  23865  cnextfvval  24073  xmeteq0  24348  imasf1oxmet  24385  comet  24526  dscmet  24585  nrmmetd  24587  tngngp  24675  tngngp3  24677  mbfsup  25699  mbfinf  25700  degltlem1  26111  logltb  26642  cxple2  26739  rlimcnp  27008  rlimcnp2  27009  isppw2  27158  sqf11  27182  slerec  27864  tgjustc1  28483  tgjustc2  28484  f1otrgitv  28878  nbuhgr2vtx1edgb  29369  dfconngr1  30207  eupth2lem3lem6  30252  nmlno0i  30813  nmlno0  30814  blocn  30826  ubth  30892  hvsubeq0  31087  hvaddcan  31089  hvsubadd  31096  normsub0  31155  hlim2  31211  pjoc1  31453  pjoc2  31458  chne0  31513  chsscon3  31519  chlejb1  31531  chnle  31533  h1de2ci  31575  elspansn  31585  elspansn2  31586  cmbr3  31627  cmcm  31633  cmcm3  31634  pjch1  31689  pjch  31713  pj11  31733  pjnel  31745  eigorth  31857  elnlfn  31947  nmlnop0  32017  lnopeq  32028  lnopcon  32054  lnfncon  32075  pjdifnormi  32186  chrelat2  32389  cvexch  32393  mdsym  32431  eqelbid  32494  fmptcof2  32667  mgcoval  32976  mgcval  32977  mgccole1  32980  mgccole2  32981  mgcmnt1  32982  mgcmnt2  32983  mgccnv  32989  unitprodclb  33417  ist0cld  33832  zarclssn  33872  zart0  33878  signswch  34576  fnrelpredd  35103  cvmlift2lem12  35319  cvmlift2lem13  35320  satfv1lem  35367  satf0op  35382  fmlafvel  35390  abs2sqle  35685  abs2sqlt  35686  axextdist  35800  brimageg  35928  brdomaing  35936  brrangeg  35937  elhf2  36176  nn0prpwlem  36323  nn0prpw  36324  onsuct0  36442  bj-sbceqgALT  36903  bj-elabd2ALT  36926  eleq2w2ALT  37048  dfgcd3  37325  cbveud  37373  wl-3xorbi123d  37476  matunitlindf  37625  prdsbnd2  37802  isdrngo1  37963  eqrelf  38256  elsymrels5  38557  dfdisjs5  38713  eldisjs5  38727  mpets2  38842  pets  38853  lsatcmp  39004  llnexchb2  39871  lautset  40084  lautle  40086  sticksstones2  42148  aks6d1c7  42185  dvdsexpnn0  42369  eu6w  42686  abbibw  42687  zindbi  42958  wepwsolem  43054  aomclem8  43073  onsupmaxb  43251  oaordnr  43309  omnord1  43318  oenord1  43329  ntrneik13  44111  ntrneix13  44112  ntrneik4w  44113  2sbc6g  44434  2sbc5g  44435  modelaxreplem3  44997  wessf1ornlem  45190  fourierdlem31  46153  fourierdlem42  46164  fourierdlem54  46175  funressndmafv2rn  47235  dfatbrafv2b  47257  fnbrafv2b  47260  ichbidv  47440  ichnfim  47451  sprsymrelf  47482  sprsymrelfo  47484  isuspgrimlem  47874  line2ylem  48672  line2xlem  48674  mofeu  48757  tposres0  48777  catprslem  48899