Theorem sylbir 236

Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
sylbir.1	⊢ (𝜓 ↔ 𝜑)
sylbir.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
sylbir	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbir

Step	Hyp	Ref	Expression
1		sylbir.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 229	. 2 ⊢ (𝜑 → 𝜓)
3		sylbir.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 17	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  3imtr3i  292  ex  413  3expa  1124  3ori  1432  an42ds  1497  nanass  1517  19.38  1846  19.35  1884  19.8aw  2059  equsexv  2280  sbi2  2313  nfeqf2  2385  equsex  2426  dfmoeu  2539  2mo  2652  axie2  2706  necon1bi  2962  necon1i  2967  r19.35  3097  spc2ed  3539  reu6  3667  rabssrabd  4014  uneqin  4217  difin0ss  4301  inelcm  4393  falseral0OLD  4443  raaan2  4450  difprsn1  4733  tppreqb  4738  n0snor2el  4764  unissint  4902  intminss  4904  dfiun2g  4959  iununi  5028  triin  5196  bm1.3iiOLD  5224  eusv2nf  5324  reusv3i  5333  axprglem  5365  axprg  5366  moabexOLD  5398  opelopabt  5474  eqrelrel  5740  opeliunxp2  5780  opelrn  5885  ssxpb  6125  xpima  6133  xpimasn  6136  dmsn0el  6162  relcnvtr  6219  relcoi2  6228  elsnxp  6242  reuop  6244  iotanul  6465  f1imadifssran  6571  dffv2  6922  fnfvrnss  7062  fressnfv  7103  fconst5  7150  f1mpt  7205  isocnv3  7276  f1owe  7297  ovprc  7394  fvmpopr2d  7518  onminesb  7736  onminsb  7737  onintrab  7739  onnminsb  7742  ordsuci  7751  onsucuni2  7774  tfindsg2  7802  zfrep6OLD  7897  fo1stres  7957  fo2ndres  7958  bropopvvv  8029  bropfvvvv  8031  frxp  8066  poseq  8098  soseq  8099  opeliunxp2f  8150  mpoxopoveqd  8161  reldmtpos  8174  frrlem4  8229  tfrlem5  8309  tfrlem9  8314  tfr2  8327  rdgsuc  8353  oaordi  8471  oeordi  8513  omopthi  8587  on2recsov  8594  fvmptmap  8819  mptelixpg  8873  ener  8938  domtr  8944  unen  8982  undom  8993  dom0  9033  xpf1o  9067  mapen  9069  pssnn  9093  unfi  9095  ssfi  9097  ensymfib  9108  entrfil  9109  enfii  9110  domtrfil  9116  unxpdomlem3  9158  isinf  9165  frfi  9185  unblem1  9192  fofinf1o  9232  fsuppun  9290  elirrvOLD  9503  inf3lem2  9541  inf3lem5  9544  cantnfp1lem1  9590  cantnfp1lem3  9592  tcmin  9651  setinds  9661  frr2  9675  r1ordg  9693  r1ord  9695  rankr1ai  9713  r1val3  9753  bndrank  9756  unbndrank  9757  rankr1b  9779  rankxplim3  9796  tcrank  9799  xpnum  9866  cardmin2  9914  infxpenlem  9926  fseqen  9940  dfac8clem  9945  alephsson  10013  alephfp  10021  dfac4  10035  kmlem6  10069  kmlem8  10071  kmlem9  10072  cflem  10158  infpssr  10221  fin1a2lem12  10324  axcc4  10352  axcc4dom  10354  ac6s2  10399  zornn0g  10418  cardidg  10461  unsnen  10466  pwcfsdom  10497  cfpwsdom  10498  gchpwdom  10584  r1tskina  10696  intgru  10728  indpi  10821  nqereu  10843  supsrlem  11025  letrii  11262  dfnn3  12179  zaddcl  12558  nn0ind  12615  fnn0ind  12619  ublbneg  12874  nn01to3  12882  infmrp1  13288  fz0  13484  fzo1fzo0n0  13661  elfzom1elp1fzo  13678  fzo0end  13704  elfznelfzo  13719  fzind2  13734  injresinjlem  13736  fleqceilz  13804  nnsinds  13941  nn0sinds  13942  faclbnd4lem1  14246  hashinf  14288  hasheqf1oi  14304  hashgt0elex  14354  hashgt23el  14377  hashfacen  14407  hash2prde  14423  hash2sspr  14442  fun2dmnop0  14457  iswrddm0  14491  swrdnnn0nd  14610  swrdnd0  14611  swrdlsw  14621  pfxn0  14640  pfxnd0  14642  swrdswrdlem  14657  pfxccatin12lem3  14685  pfxccat3  14687  pfxccat3a  14691  swrdccat3blem  14692  cshwsublen  14749  cshwidxmod  14756  repswcshw  14765  cshw1  14775  trclun  14967  dmtrclfv  14971  rediv  15084  imdiv  15091  fsump1i  15722  modfsummods  15747  bpolydiflem  16010  bpoly3  16014  bpoly4  16015  cos1bnd  16145  sinltx  16147  rpnnen2lem1  16172  rpnnen2lem2  16173  rpnnen2lem12  16183  odd2np1  16301  opoe  16323  omoe  16324  opeo  16325  omeo  16326  gcdcllem1  16459  gcdaddmlem  16484  dfgcd2  16506  algfx  16540  lcmledvds  16559  lcmfunsnlem  16601  lcmfun  16605  coprmprod  16621  coprmproddvdslem  16622  odzval  16753  odzdvds  16757  prmreclem5  16882  mul4sq  16916  prmgaplem5  17017  prmgaplem6  17018  imasaddfnlem  17483  mreexexlem4d  17604  joindmss  18334  meetdmss  18348  gictr  19242  cntzval  19287  symg2bas  19359  odfval  19498  efgsfo  19705  efgrelexlemb  19716  dprddomcld  19969  dprdsubg  19992  dprd2da  20010  lssacs  20957  cnfldinv  21378  pzriprnglem7  21462  ocvval  21642  selvval  22096  dmatmul  22480  mdetfval1  22573  mndifsplit  22619  fvmptnn04if  22832  toprntopon  22908  opnnei  23103  ordtbas2  23174  ordtrest2lem  23186  lmmo  23363  fincmp  23376  bwth  23393  txbas  23550  ptcnplem  23604  tx2ndc  23634  hmphtr  23766  fbun  23823  filconn  23866  ptcmplem5  24039  cnextcn  24050  utoptop  24217  ucncn  24267  metust  24541  cfilucfil  24542  elcncf1di  24880  xrhmeo  24931  phtpycc  24976  copco  25003  pcohtpylem  25004  pcopt  25007  pcopt2  25008  ncvsi  25136  ovolval  25458  iunmbl2  25542  itg2splitlem  25733  cpnfval  25917  plyval  26176  fta1  26292  aaliou2b  26325  tayl0  26345  ulmdvlem3  26385  radcnvlem2  26397  dvradcnv  26404  reeff1o  26430  sincosq1lem  26479  sincosq2sgn  26481  sincosq4sgn  26483  sinq12ge0  26490  logrncl  26549  eflog  26558  cxpge0  26665  logb1  26751  atanf  26862  atanbnd  26908  igamf  27032  igamcl  27033  lgsne0  27316  mul2sq  27400  2sqreultblem  27429  pntibnd  27574  ostth  27620  nobdaymin  27763  nocvxminlem  27764  cutlt  27942  norec2ov  27967  addsuniflem  28011  mulsuniflem  28159  oldfib  28387  zmulscld  28407  zseo  28432  z12addscl  28487  mpteleeOLD  28982  axlowdimlem9  29037  axlowdimlem12  29040  axcontlem2  29052  axcontlem12  29062  structgrssvtx  29111  structgrssiedg  29112  lpvtx  29155  nbuhgr  29430  nbumgr  29434  nbuhgr2vtx1edgblem  29438  nbgr0edglem  29443  nbgr1vtx  29445  uvtx01vtx  29484  prcliscplgr  29501  cusgrsizeinds  29539  sizusglecusglem2  29549  uhgrvd00  29621  fusgrregdegfi  29656  rusgr1vtxlem  29674  wlkeq  29720  wlk1walk  29725  uspgr2wlkeq  29732  wlklenvclwlk  29740  wlkreslem  29754  wlkdlem2  29768  wlkdlem4  29770  spthonepeq  29838  cyclnumvtx  29886  clwlkclwwlkflem  30092  clwlkclwwlkfolem  30095  clwlkclwwlkf  30096  clwwisshclwws  30103  clwwlkneq0  30117  3wlkdlem6  30253  eupth2eucrct  30305  eupth2lem1  30306  eupth2lem3lem7  30322  frgr3vlem1  30361  frgr3vlem2  30362  frgrncvvdeqlem8  30394  frgrncvvdeqlem9  30395  numclwwlk5  30476  frgrreg  30482  frgrregord013  30483  friendshipgt3  30486  isgrpo  30586  vciOLD  30650  vcex  30667  nmogtmnf  30859  siilem1  30940  siii  30942  ajmoi  30947  bcsiALT  31268  hhcms  31292  ocval  31369  hsupval  31423  omlsilem  31491  h1de2bi  31643  h1de2ctlem  31644  hosubeq0i  31915  adjmo  31921  nmopgtmnf  31957  nlfnval  31970  nmcopex  32118  nmcfnex  32142  riesz4i  32152  riesz1  32154  riesz2  32155  opsqrlem1  32229  superpos  32443  hatomistici  32451  chpssati  32452  mdsymlem3  32494  3o1cs  32548  3o2cs  32549  3o3cs  32550  iunrnmptss  32654  brabgaf  32698  f1mptrn  32727  ffsrn  32820  xnn0gt0  32861  hashxpe  32899  sgn3da  32926  elrgspnlem4  33326  prmidl2  33524  mxidlnzrb  33563  evl1deg2  33660  evl1deg3  33661  fedgmul  33815  cos9thpiminplylem2  33967  ordtrest2NEWlem  34106  qqhval2  34166  esumfsup  34254  esumcvg  34270  cntnevol  34412  ddemeas  34420  dya2icoseg2  34462  dya2iocnei  34466  eulerpartlems  34544  eulerpartlemgvv  34560  eulerpart  34566  cndprobprob  34622  ballotlemsdom  34696  ballotth  34722  bnj945  34956  bnj1379  35012  bnj1459  35025  bnj557  35083  bnj571  35088  bnj849  35107  bnj964  35125  bnj978  35131  bnj1018g  35145  bnj1018  35146  bnj1020  35147  bnj1033  35151  bnj1175  35186  bnj1398  35216  bnj1417  35223  bnj1523  35253  nummin  35274  r1omhf  35287  axprALT2  35290  fineqvnttrclselem1  35302  onvf1odlem4  35334  onvf1od  35335  cusgr3cyclex  35364  txpconn  35460  satfv1  35591  satffun  35637  msubco  35759  mclsax  35797  dfon2lem7  36015  dfon2lem8  36016  pprodss4v  36110  fullfunfv  36175  altxpsspw  36205  funtransport  36259  fvtransport  36260  funray  36368  fvray  36369  funline  36370  fvline  36372  finminlem  36546  bisym1  36647  onsucconni  36665  onsucsuccmpi  36671  weiunse  36696  bj-currypara  36870  bj-cbvaw  36981  axc11n11r  37026  bj-equsal2  37178  bj-xpima1snALT  37310  bj-unexg  37391  bj-bm1.3ii  37417  bj-axseprep  37427  bj-axreprepsep  37428  bj-opelidb1ALT  37526  mptsnunlem  37700  iooelexlt  37724  relowlpssretop  37726  rdgeqoa  37732  difunieq  37736  nlpineqsn  37770  fvineqsneq  37774  wl-ax12v2cl  37868  wl-lem-nexmo  37938  matunitlindflem1  37983  ptrecube  37987  poimirlem26  38013  poimirlem30  38017  poimir  38020  ismblfin  38028  itg2addnclem  38038  dvasin  38071  sdclem2  38109  totbndbnd  38156  ismgmOLD  38217  exidresid  38246  isrngo  38264  rngoablo2  38276  rngoueqz  38307  isdivrngo  38317  isdrngo1  38323  isdrngo2  38325  ispridl2  38405  relcnveq3  38694  elrelscnveq3  38994  disjimeceqim  39171  dmqsblocks  39334  ax12eq  39433  ax12el  39434  lkr0f  39586  hl2at  39897  dalemswapyz  40148  pclfinclN  40442  osumcllem11N  40458  pexmidlem8N  40469  ltrnnid  40628  aks4d1p8  42572  redvmptabs  42837  sn-00id  42878  rictr  43006  eu6w  43126  mptfcl  43169  fphpd  43261  elmnc  43581  itgoval  43606  arearect  43660  reabsifpos  44078  clsk3nimkb  44484  grumnud  44730  nanorxor  44749  pm11.71  44841  iotavalsb  44877  sbiota1  44878  2uasbanh  45005  eel0TT  45147  eelT00  45148  eelTTT  45149  eelT11  45150  eelT12  45152  eelTT1  45153  eelT01  45154  eel0T1  45155  eelTT  45214  uunT1p1  45224  uun121  45226  uun121p1  45227  un2122  45233  uunTT1  45236  uunTT1p1  45237  uunTT1p2  45238  uunT11  45239  uunT11p1  45240  uunT11p2  45241  uunT12  45242  uunT12p1  45243  uunT12p2  45244  uunT12p3  45245  uunT12p4  45246  uunT12p5  45247  uun111  45248  3anidm12p2  45250  uun123  45251  3impdirp1  45259  undif3VD  45325  ax6e2ndeqVD  45352  2uasbanhVD  45354  ax6e2ndeqALT  45374  iunconnlem2  45378  sineq0ALT  45380  modelaxreplem1  45422  permaxrep  45450  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  stoweidlem3  46446  stoweidlem17  46460  fourierdlem42  46592  fourierdlem48  46597  fourierdlem50  46599  fourierdlem51  46600  fourierdlem76  46625  fourierdlem83  46632  fourierdlem87  46636  hoidmvval0  47030  evenwodadd  47332  rexrsb  47563  2reu8i  47576  2reuimp  47578  afv0nbfvbi  47614  afvfv0bi  47615  afveu  47616  fnbrafvb  47617  afvres  47635  tz6.12-afv  47636  dmfcoafv  47638  afvco2  47639  aovprc  47651  aovrcl  47652  aovmpt4g  47664  afv2eu  47701  afv2res  47702  tz6.12-afv2  47703  tz6.12i-afv2  47706  afv2rnfveq  47725  fvmptrab  47755  fvmptrabdm  47756  fzopred  47786  2ffzoeq  47791  muldvdsfacm1  47850  elsprel  47950  prproropf1o  47982  reupr  47997  lighneal  48089  odd2prm2  48209  even3prm2  48210  grictr  48414  grlimgrtrilem2  48493  usgrexmpl12ngric  48529  gpgprismgr4cycllem8  48593  gpgprismgr4cycllem11  48596  pgnbgreunbgrlem2lem1  48605  upgrwlkupwlk  48631  ovn0ssdmfun  48650  islinindfis  48940  rrx2linest  49233  line2ylem  49242  mofeu  49338  homf0  49499  uobffth  49708  uobeqw  49709  initopropd  49733  termopropd  49734  zeroopropd  49735  fucofvalne  49815  isthincd2  49927  lanrcl  50111  ranrcl  50112  setrec2fun  50182  elsetrecslem  50189  setrecsres  50192  secval  50237  cscval  50238  cotval  50239