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  nalset  5248  opthg  5423  opelopabsb  5476  isso2i  5567  opeliunxp2  5785  resieq  5947  dfpo2  6252  cbviotaw  6453  cbviota  6455  iota2df  6477  fnbrfvb  6882  fvelimab  6904  fvopab5  6973  fmptco  7074  fsng  7082  fressnfv  7105  fnpr2g  7156  isorel  7272  isocnv  7276  isocnv3  7278  isotr  7282  eqfunresadj  7306  ovg  7523  caovcang  7559  caovordg  7565  caovord3d  7568  caovord  7569  caofidlcan  7660  orduninsuc  7785  xpord2pred  8086  xpord3pred  8093  opeliunxp2f  8151  brtpos  8176  dftpos4  8186  omopth  8589  ecopovsym  8757  xpf1o  9068  nneneq  9131  ttrclselem2  9636  r1pwALT  9759  karden  9808  infxpenlem  9924  aceq0  10029  cflim2  10174  zfac  10371  ttukeylem1  10420  axextnd  10503  axrepndlem1  10504  axrepndlem2  10505  axrepnd  10506  axacndlem5  10523  zfcndrep  10526  zfcndac  10531  winalim  10607  gruina  10730  ltrnq  10891  ltsosr  11006  ltasr  11012  axpre-lttri  11077  axpre-ltadd  11079  nn0sub  12476  zextle  12591  zextlt  12592  xlesubadd  13204  sqeqor  14167  nn0opth2  14223  rexfiuz  15299  climshft  15527  rpnnen2lem10  16179  dvdsext  16279  ltoddhalfle  16319  halfleoddlt  16320  sumodd  16346  sadcadd  16416  dvdssq  16525  rpexp  16681  pcdvdsb  16829  imasleval  17494  isacs2  17608  acsfiel  17609  funcres2b  17853  pospropd  18280  isnsg  19119  nsgbi  19121  elnmz  19127  nmzbi  19128  oddvdsnn0  19508  odeq  19514  odmulg  19520  isslw  19572  slwispgp  19575  gsumval3lem2  19870  gsumcom2  19939  abveq0  20784  cnt0  23320  kqfvima  23704  kqt0lem  23710  isr0  23711  r0cld  23712  regr1lem2  23714  nrmr0reg  23723  isfildlem  23831  cnextfvval  24039  xmeteq0  24312  imasf1oxmet  24349  comet  24487  dscmet  24546  nrmmetd  24548  tngngp  24628  tngngp3  24630  mbfsup  25640  mbfinf  25641  degltlem1  26049  logltb  26580  cxple2  26677  rlimcnp  26946  rlimcnp2  26947  isppw2  27096  sqf11  27120  lesrec  27810  tgjustc1  28562  tgjustc2  28563  f1otrgitv  28957  nbuhgr2vtx1edgb  29440  dfconngr1  30278  eupth2lem3lem6  30323  nmlno0i  30885  nmlno0  30886  blocn  30898  ubth  30964  hvsubeq0  31159  hvaddcan  31161  hvsubadd  31168  normsub0  31227  hlim2  31283  pjoc1  31525  pjoc2  31530  chne0  31585  chsscon3  31591  chlejb1  31603  chnle  31605  h1de2ci  31647  elspansn  31657  elspansn2  31658  cmbr3  31699  cmcm  31705  cmcm3  31706  pjch1  31761  pjch  31785  pj11  31805  pjnel  31817  eigorth  31929  elnlfn  32019  nmlnop0  32089  lnopeq  32100  lnopcon  32126  lnfncon  32147  pjdifnormi  32258  chrelat2  32461  cvexch  32465  mdsym  32503  eqelbid  32564  fmptcof2  32750  mgcoval  33066  mgcval  33067  mgccole1  33070  mgccole2  33071  mgcmnt1  33072  mgcmnt2  33073  mgccnv  33079  domnprodeq0  33357  unitprodclb  33469  ist0cld  33998  zarclssn  34038  zart0  34044  signswch  34726  fnrelpredd  35255  r1omhfb  35277  r1omhfbregs  35302  cvmlift2lem12  35517  cvmlift2lem13  35518  satfv1lem  35565  satf0op  35580  fmlafvel  35588  abs2sqle  35883  abs2sqlt  35884  axextdist  36000  brimageg  36128  brdomaing  36136  brrangeg  36137  elhf2  36378  nn0prpwlem  36525  nn0prpw  36526  onsuct0  36644  ttcwf2  36728  bj-sbceqgALT  37222  bj-elabd2ALT  37245  eleq2w2ALT  37367  bj-axseprep  37394  dfgcd3  37651  cbveud  37699  wl-3xorbi123d  37802  wl-dfcleq  37841  matunitlindf  37950  prdsbnd2  38127  isdrngo1  38288  eqrelf  38590  elsymrels5  38972  dfdisjs5  39129  eldisjs5  39155  mpets2  39287  pets  39298  lsatcmp  39460  llnexchb2  40326  lautset  40539  lautle  40541  sticksstones2  42597  aks6d1c7  42634  dvdsexpnn0  42777  eu6w  43120  abbibw  43121  zindbi  43389  wepwsolem  43485  aomclem8  43504  onsupmaxb  43682  oaordnr  43739  omnord1  43748  oenord1  43759  ntrneik13  44540  ntrneix13  44541  ntrneik4w  44542  2sbc6g  44857  2sbc5g  44858  modelaxreplem3  45422  wessf1ornlem  45630  fourierdlem31  46581  fourierdlem42  46592  fourierdlem54  46603  funressndmafv2rn  47668  dfatbrafv2b  47690  fnbrafv2b  47693  ichbidv  47910  ichnfim  47921  sprsymrelf  47952  sprsymrelfo  47954  isuspgrimlem  48368  line2ylem  49224  line2xlem  49226  mofeu  49320  tposres0  49349  catprslem  49482