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  2363  sb8eulem  2597  abbib  2804  cleqh  2864  cleqf  2927  vtoclbg  3536  vtoclb  3547  ceqsexg  3632  elabgf  3653  reu6  3709  ruOLD  3764  sbcbig  3817  unineq  4263  sbcnestgfw  4396  sbcnestgf  4401  preq12bg  4829  axrep1  5250  axrep4OLD  5256  nalset  5283  opthg  5452  opelopabsb  5505  isso2i  5598  opeliunxp2  5818  resieq  5977  dfpo2  6285  cbviotaw  6490  cbviota  6492  iota2df  6517  fnbrfvb  6928  fvelimab  6950  fvopab5  7018  fmptco  7118  fsng  7126  fressnfv  7149  fnpr2g  7201  isorel  7318  isocnv  7322  isocnv3  7324  isotr  7328  eqfunresadj  7352  ovg  7570  caovcang  7606  caovordg  7612  caovord3d  7615  caovord  7616  caofidlcan  7707  orduninsuc  7836  xpord2pred  8142  xpord3pred  8149  opeliunxp2f  8207  brtpos  8232  dftpos4  8242  omopth  8672  ecopovsym  8831  xpf1o  9151  nneneq  9218  ttrclselem2  9738  r1pwALT  9858  karden  9907  infxpenlem  10025  aceq0  10130  cflim2  10275  zfac  10472  ttukeylem1  10521  axextnd  10603  axrepndlem1  10604  axrepndlem2  10605  axrepnd  10606  axacndlem5  10623  zfcndrep  10626  zfcndac  10631  winalim  10707  gruina  10830  ltrnq  10991  ltsosr  11106  ltasr  11112  axpre-lttri  11177  axpre-ltadd  11179  nn0sub  12549  zextle  12664  zextlt  12665  xlesubadd  13277  sqeqor  14232  nn0opth2  14288  rexfiuz  15364  climshft  15590  rpnnen2lem10  16239  dvdsext  16338  ltoddhalfle  16378  halfleoddlt  16379  sumodd  16405  sadcadd  16475  dvdssq  16584  rpexp  16739  pcdvdsb  16887  imasleval  17553  isacs2  17663  acsfiel  17664  funcres2b  17908  pospropd  18335  isnsg  19136  nsgbi  19138  elnmz  19144  nmzbi  19145  oddvdsnn0  19523  odeq  19529  odmulg  19535  isslw  19587  slwispgp  19590  gsumval3lem2  19885  gsumcom2  19954  abveq0  20776  cnt0  23282  kqfvima  23666  kqt0lem  23672  isr0  23673  r0cld  23674  regr1lem2  23676  nrmr0reg  23685  isfildlem  23793  cnextfvval  24001  xmeteq0  24275  imasf1oxmet  24312  comet  24450  dscmet  24509  nrmmetd  24511  tngngp  24591  tngngp3  24593  mbfsup  25615  mbfinf  25616  degltlem1  26027  logltb  26559  cxple2  26656  rlimcnp  26925  rlimcnp2  26926  isppw2  27075  sqf11  27099  slerec  27781  tgjustc1  28400  tgjustc2  28401  f1otrgitv  28795  nbuhgr2vtx1edgb  29277  dfconngr1  30115  eupth2lem3lem6  30160  nmlno0i  30721  nmlno0  30722  blocn  30734  ubth  30800  hvsubeq0  30995  hvaddcan  30997  hvsubadd  31004  normsub0  31063  hlim2  31119  pjoc1  31361  pjoc2  31366  chne0  31421  chsscon3  31427  chlejb1  31439  chnle  31441  h1de2ci  31483  elspansn  31493  elspansn2  31494  cmbr3  31535  cmcm  31541  cmcm3  31542  pjch1  31597  pjch  31621  pj11  31641  pjnel  31653  eigorth  31765  elnlfn  31855  nmlnop0  31925  lnopeq  31936  lnopcon  31962  lnfncon  31983  pjdifnormi  32094  chrelat2  32297  cvexch  32301  mdsym  32339  eqelbid  32402  fmptcof2  32581  mgcoval  32912  mgcval  32913  mgccole1  32916  mgccole2  32917  mgcmnt1  32918  mgcmnt2  32919  mgccnv  32925  unitprodclb  33350  ist0cld  33810  zarclssn  33850  zart0  33856  signswch  34539  fnrelpredd  35066  cvmlift2lem12  35282  cvmlift2lem13  35283  satfv1lem  35330  satf0op  35345  fmlafvel  35353  abs2sqle  35648  abs2sqlt  35649  axextdist  35763  brimageg  35891  brdomaing  35899  brrangeg  35900  elhf2  36139  nn0prpwlem  36286  nn0prpw  36287  onsuct0  36405  bj-sbceqgALT  36866  bj-elabd2ALT  36889  eleq2w2ALT  37011  dfgcd3  37288  cbveud  37336  wl-3xorbi123d  37439  matunitlindf  37588  prdsbnd2  37765  isdrngo1  37926  eqrelf  38219  elsymrels5  38520  dfdisjs5  38676  eldisjs5  38690  mpets2  38805  pets  38816  lsatcmp  38967  llnexchb2  39834  lautset  40047  lautle  40049  sticksstones2  42106  aks6d1c7  42143  dvdsexpnn0  42330  eu6w  42646  abbibw  42647  zindbi  42917  wepwsolem  43013  aomclem8  43032  onsupmaxb  43210  oaordnr  43267  omnord1  43276  oenord1  43287  ntrneik13  44069  ntrneix13  44070  ntrneik4w  44071  2sbc6g  44387  2sbc5g  44388  modelaxreplem3  44953  wessf1ornlem  45157  fourierdlem31  46115  fourierdlem42  46126  fourierdlem54  46137  funressndmafv2rn  47200  dfatbrafv2b  47222  fnbrafv2b  47225  ichbidv  47415  ichnfim  47426  sprsymrelf  47457  sprsymrelfo  47459  isuspgrimlem  47856  line2ylem  48679  line2xlem  48681  mofeu  48774  tposres0  48800  catprslem  48933