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  1526  norass  1538  ru0  2132  sbbib  2363  sb8eulem  2595  abbib  2802  cleqh  2862  cleqf  2924  vtoclbg  3511  vtoclb  3521  ceqsexg  3604  elabgf  3626  reu6  3681  ruOLD  3736  sbcbig  3789  unineq  4237  sbcnestgfw  4370  sbcnestgf  4375  preq12bg  4804  axrep1  5220  axrep4OLD  5226  nalset  5253  opthg  5420  opelopabsb  5473  isso2i  5564  opeliunxp2  5782  resieq  5943  dfpo2  6248  cbviotaw  6449  cbviota  6451  iota2df  6473  fnbrfvb  6878  fvelimab  6900  fvopab5  6968  fmptco  7068  fsng  7076  fressnfv  7099  fnpr2g  7150  isorel  7266  isocnv  7270  isocnv3  7272  isotr  7276  eqfunresadj  7300  ovg  7517  caovcang  7553  caovordg  7559  caovord3d  7562  caovord  7563  caofidlcan  7654  orduninsuc  7779  xpord2pred  8081  xpord3pred  8088  opeliunxp2f  8146  brtpos  8171  dftpos4  8181  omopth  8583  ecopovsym  8749  xpf1o  9059  nneneq  9122  ttrclselem2  9623  r1pwALT  9746  karden  9795  infxpenlem  9911  aceq0  10016  cflim2  10161  zfac  10358  ttukeylem1  10407  axextnd  10489  axrepndlem1  10490  axrepndlem2  10491  axrepnd  10492  axacndlem5  10509  zfcndrep  10512  zfcndac  10517  winalim  10593  gruina  10716  ltrnq  10877  ltsosr  10992  ltasr  10998  axpre-lttri  11063  axpre-ltadd  11065  nn0sub  12438  zextle  12552  zextlt  12553  xlesubadd  13164  sqeqor  14125  nn0opth2  14181  rexfiuz  15257  climshft  15485  rpnnen2lem10  16134  dvdsext  16234  ltoddhalfle  16274  halfleoddlt  16275  sumodd  16301  sadcadd  16371  dvdssq  16480  rpexp  16635  pcdvdsb  16783  imasleval  17447  isacs2  17561  acsfiel  17562  funcres2b  17806  pospropd  18233  isnsg  19069  nsgbi  19071  elnmz  19077  nmzbi  19078  oddvdsnn0  19458  odeq  19464  odmulg  19470  isslw  19522  slwispgp  19525  gsumval3lem2  19820  gsumcom2  19889  abveq0  20735  cnt0  23262  kqfvima  23646  kqt0lem  23652  isr0  23653  r0cld  23654  regr1lem2  23656  nrmr0reg  23665  isfildlem  23773  cnextfvval  23981  xmeteq0  24254  imasf1oxmet  24291  comet  24429  dscmet  24488  nrmmetd  24490  tngngp  24570  tngngp3  24572  mbfsup  25593  mbfinf  25594  degltlem1  26005  logltb  26537  cxple2  26634  rlimcnp  26903  rlimcnp2  26904  isppw2  27053  sqf11  27077  slerec  27761  tgjustc1  28454  tgjustc2  28455  f1otrgitv  28849  nbuhgr2vtx1edgb  29332  dfconngr1  30170  eupth2lem3lem6  30215  nmlno0i  30776  nmlno0  30777  blocn  30789  ubth  30855  hvsubeq0  31050  hvaddcan  31052  hvsubadd  31059  normsub0  31118  hlim2  31174  pjoc1  31416  pjoc2  31421  chne0  31476  chsscon3  31482  chlejb1  31494  chnle  31496  h1de2ci  31538  elspansn  31548  elspansn2  31549  cmbr3  31590  cmcm  31596  cmcm3  31597  pjch1  31652  pjch  31676  pj11  31696  pjnel  31708  eigorth  31820  elnlfn  31910  nmlnop0  31980  lnopeq  31991  lnopcon  32017  lnfncon  32038  pjdifnormi  32149  chrelat2  32352  cvexch  32356  mdsym  32394  eqelbid  32456  fmptcof2  32641  mgcoval  32974  mgcval  32975  mgccole1  32978  mgccole2  32979  mgcmnt1  32980  mgcmnt2  32981  mgccnv  32987  unitprodclb  33361  ist0cld  33867  zarclssn  33907  zart0  33913  signswch  34595  fnrelpredd  35123  r1omhfb  35144  r1omhfbregs  35154  cvmlift2lem12  35379  cvmlift2lem13  35380  satfv1lem  35427  satf0op  35442  fmlafvel  35450  abs2sqle  35745  abs2sqlt  35746  axextdist  35862  brimageg  35990  brdomaing  35998  brrangeg  35999  elhf2  36240  nn0prpwlem  36387  nn0prpw  36388  onsuct0  36506  bj-sbceqgALT  36967  bj-elabd2ALT  36990  eleq2w2ALT  37112  dfgcd3  37389  cbveud  37437  wl-3xorbi123d  37540  matunitlindf  37678  prdsbnd2  37855  isdrngo1  38016  eqrelf  38312  elsymrels5  38672  dfdisjs5  38830  eldisjs5  38844  mpets2  38959  pets  38970  lsatcmp  39122  llnexchb2  39988  lautset  40201  lautle  40203  sticksstones2  42260  aks6d1c7  42297  dvdsexpnn0  42452  eu6w  42794  abbibw  42795  zindbi  43063  wepwsolem  43159  aomclem8  43178  onsupmaxb  43356  oaordnr  43413  omnord1  43422  oenord1  43433  ntrneik13  44215  ntrneix13  44216  ntrneik4w  44217  2sbc6g  44532  2sbc5g  44533  modelaxreplem3  45097  wessf1ornlem  45306  fourierdlem31  46260  fourierdlem42  46271  fourierdlem54  46282  funressndmafv2rn  47347  dfatbrafv2b  47369  fnbrafv2b  47372  ichbidv  47577  ichnfim  47588  sprsymrelf  47619  sprsymrelfo  47621  isuspgrimlem  48019  line2ylem  48876  line2xlem  48878  mofeu  48972  tposres0  49001  catprslem  49135