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  641  xorbi12d  1527  norass  1539  ru0  2133  sbbib  2366  sb8eulem  2599  abbib  2806  cleqh  2866  cleqf  2928  vtoclbg  3503  vtoclb  3513  ceqsexg  3596  elabgf  3618  reu6  3673  ruOLD  3728  sbcbig  3781  unineq  4229  sbcnestgfw  4362  sbcnestgf  4367  preq12bg  4797  axrep1  5213  axrep4OLD  5219  nalsetOLD  5250  opthg  5425  opelopabsb  5478  isso2i  5569  opeliunxp2  5787  resieq  5949  dfpo2  6254  cbviotaw  6455  cbviota  6457  iota2df  6479  fnbrfvb  6884  fvelimab  6906  fvopab5  6975  fmptco  7076  fsng  7084  fressnfv  7107  fnpr2g  7158  isorel  7274  isocnv  7278  isocnv3  7280  isotr  7284  eqfunresadj  7308  ovg  7525  caovcang  7561  caovordg  7567  caovord3d  7570  caovord  7571  caofidlcan  7662  orduninsuc  7787  xpord2pred  8088  xpord3pred  8095  opeliunxp2f  8153  brtpos  8178  dftpos4  8188  omopth  8591  ecopovsym  8759  xpf1o  9070  nneneq  9133  ttrclselem2  9638  r1pwALT  9761  karden  9810  infxpenlem  9926  aceq0  10031  cflim2  10176  zfac  10373  ttukeylem1  10422  axextnd  10505  axrepndlem1  10506  axrepndlem2  10507  axrepnd  10508  axacndlem5  10525  zfcndrep  10528  zfcndac  10533  winalim  10609  gruina  10732  ltrnq  10893  ltsosr  11008  ltasr  11014  axpre-lttri  11079  axpre-ltadd  11081  nn0sub  12478  zextle  12593  zextlt  12594  xlesubadd  13206  sqeqor  14169  nn0opth2  14225  rexfiuz  15301  climshft  15529  rpnnen2lem10  16181  dvdsext  16281  ltoddhalfle  16321  halfleoddlt  16322  sumodd  16348  sadcadd  16418  dvdssq  16527  rpexp  16683  pcdvdsb  16831  imasleval  17496  isacs2  17610  acsfiel  17611  funcres2b  17855  pospropd  18282  isnsg  19121  nsgbi  19123  elnmz  19129  nmzbi  19130  oddvdsnn0  19510  odeq  19516  odmulg  19522  isslw  19574  slwispgp  19577  gsumval3lem2  19872  gsumcom2  19941  abveq0  20786  cnt0  23321  kqfvima  23705  kqt0lem  23711  isr0  23712  r0cld  23713  regr1lem2  23715  nrmr0reg  23724  isfildlem  23832  cnextfvval  24040  xmeteq0  24313  imasf1oxmet  24350  comet  24488  dscmet  24547  nrmmetd  24549  tngngp  24629  tngngp3  24631  mbfsup  25641  mbfinf  25642  degltlem1  26047  logltb  26577  cxple2  26674  rlimcnp  26942  rlimcnp2  26943  isppw2  27092  sqf11  27116  lesrec  27805  tgjustc1  28557  tgjustc2  28558  f1otrgitv  28952  nbuhgr2vtx1edgb  29435  dfconngr1  30273  eupth2lem3lem6  30318  nmlno0i  30880  nmlno0  30881  blocn  30893  ubth  30959  hvsubeq0  31154  hvaddcan  31156  hvsubadd  31163  normsub0  31222  hlim2  31278  pjoc1  31520  pjoc2  31525  chne0  31580  chsscon3  31586  chlejb1  31598  chnle  31600  h1de2ci  31642  elspansn  31652  elspansn2  31653  cmbr3  31694  cmcm  31700  cmcm3  31701  pjch1  31756  pjch  31780  pj11  31800  pjnel  31812  eigorth  31924  elnlfn  32014  nmlnop0  32084  lnopeq  32095  lnopcon  32121  lnfncon  32142  pjdifnormi  32253  chrelat2  32456  cvexch  32460  mdsym  32498  eqelbid  32559  fmptcof2  32745  mgcoval  33061  mgcval  33062  mgccole1  33065  mgccole2  33066  mgcmnt1  33067  mgcmnt2  33068  mgccnv  33074  domnprodeq0  33352  unitprodclb  33464  ist0cld  33993  zarclssn  34033  zart0  34039  signswch  34721  fnrelpredd  35250  r1omhfb  35272  r1omhfbregs  35297  cvmlift2lem12  35512  cvmlift2lem13  35513  satfv1lem  35560  satf0op  35575  fmlafvel  35583  abs2sqle  35878  abs2sqlt  35879  axextdist  35995  brimageg  36123  brdomaing  36131  brrangeg  36132  elhf2  36373  nn0prpwlem  36520  nn0prpw  36521  onsuct0  36639  ttcwf2  36723  bj-sbceqgALT  37225  bj-elabd2ALT  37248  eleq2w2ALT  37370  bj-axseprep  37397  dfgcd3  37654  cbveud  37702  wl-3xorbi123d  37805  wl-dfcleq  37844  matunitlindf  37953  prdsbnd2  38130  isdrngo1  38291  eqrelf  38593  elsymrels5  38975  dfdisjs5  39132  eldisjs5  39158  mpets2  39290  pets  39301  lsatcmp  39463  llnexchb2  40329  lautset  40542  lautle  40544  sticksstones2  42600  aks6d1c7  42637  dvdsexpnn0  42780  eu6w  43123  abbibw  43124  zindbi  43392  wepwsolem  43488  aomclem8  43507  onsupmaxb  43685  oaordnr  43742  omnord1  43751  oenord1  43762  ntrneik13  44543  ntrneix13  44544  ntrneik4w  44545  2sbc6g  44860  2sbc5g  44861  modelaxreplem3  45425  wessf1ornlem  45633  fourierdlem31  46584  fourierdlem42  46595  fourierdlem54  46606  funressndmafv2rn  47683  dfatbrafv2b  47705  fnbrafv2b  47708  ichbidv  47925  ichnfim  47936  sprsymrelf  47967  sprsymrelfo  47969  isuspgrimlem  48383  line2ylem  49239  line2xlem  49241  mofeu  49335  tposres0  49364  catprslem  49497