Theorem sylbir 235

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 228	. 2 ⊢ (𝜑 → 𝜓)
3		sylbir.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 17	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:  3imtr3i  291  ex  412  3expa  1119  3ori  1427  an42ds  1492  nanass  1512  19.38  1841  19.35  1879  19.8aw  2054  equsexv  2276  sbi2  2309  nfeqf2  2381  equsex  2422  dfmoeu  2535  2mo  2648  axie2  2703  necon1bi  2960  necon1i  2965  r19.35  3095  spc2ed  3543  reu6  3672  rabssrabd  4023  uneqin  4229  difin0ss  4313  inelcm  4405  falseral0OLD  4455  raaan2  4462  difprsn1  4745  tppreqb  4750  n0snor2el  4776  unissint  4914  intminss  4916  dfiun2g  4972  iununi  5041  triin  5209  bm1.3iiOLD  5237  eusv2nf  5337  reusv3i  5346  axprglem  5378  axprg  5379  moabexOLD  5411  opelopabt  5487  eqrelrel  5753  opeliunxp2  5793  opelrn  5898  ssxpb  6138  xpima  6146  xpimasn  6149  dmsn0el  6175  relcnvtr  6232  relcoi2  6241  elsnxp  6255  reuop  6257  iotanul  6478  f1imadifssran  6584  dffv2  6935  fnfvrnss  7073  fressnfv  7114  fconst5  7161  f1mpt  7216  isocnv3  7287  f1owe  7308  ovprc  7405  fvmpopr2d  7529  onminesb  7747  onminsb  7748  onintrab  7750  onnminsb  7753  ordsuci  7762  onsucuni2  7785  tfindsg2  7813  zfrep6OLD  7908  fo1stres  7968  fo2ndres  7969  bropopvvv  8040  bropfvvvv  8042  frxp  8076  poseq  8108  soseq  8109  opeliunxp2f  8160  mpoxopoveqd  8171  reldmtpos  8184  frrlem4  8239  tfrlem5  8319  tfrlem9  8324  tfr2  8337  rdgsuc  8363  oaordi  8481  oeordi  8523  omopthi  8597  on2recsov  8604  fvmptmap  8829  mptelixpg  8883  ener  8948  domtr  8954  unen  8992  undom  9003  dom0  9043  xpf1o  9077  mapen  9079  pssnn  9103  unfi  9105  ssfi  9107  ensymfib  9118  entrfil  9119  enfii  9120  domtrfil  9126  unxpdomlem3  9168  isinf  9175  frfi  9195  unblem1  9202  fofinf1o  9242  fsuppun  9300  elirrv  9512  inf3lem2  9550  inf3lem5  9553  cantnfp1lem1  9599  cantnfp1lem3  9601  tcmin  9660  setinds  9670  frr2  9684  r1ordg  9702  r1ord  9704  rankr1ai  9722  r1val3  9762  bndrank  9765  unbndrank  9766  rankr1b  9788  rankxplim3  9805  tcrank  9808  xpnum  9875  cardmin2  9923  infxpenlem  9935  fseqen  9949  dfac8clem  9954  alephsson  10022  alephfp  10030  dfac4  10044  kmlem6  10078  kmlem8  10080  kmlem9  10081  cflem  10167  infpssr  10230  fin1a2lem12  10333  axcc4  10361  axcc4dom  10363  ac6s2  10408  zornn0g  10427  cardidg  10470  unsnen  10475  pwcfsdom  10506  cfpwsdom  10507  gchpwdom  10593  r1tskina  10705  intgru  10737  indpi  10830  nqereu  10852  supsrlem  11034  letrii  11271  dfnn3  12188  zaddcl  12567  nn0ind  12624  fnn0ind  12628  ublbneg  12883  nn01to3  12891  infmrp1  13297  fz0  13493  fzo1fzo0n0  13670  elfzom1elp1fzo  13687  fzo0end  13713  elfznelfzo  13728  fzind2  13743  injresinjlem  13745  fleqceilz  13813  nnsinds  13950  nn0sinds  13951  faclbnd4lem1  14255  hashinf  14297  hasheqf1oi  14313  hashgt0elex  14363  hashgt23el  14386  hashfacen  14416  hash2prde  14432  hash2sspr  14451  fun2dmnop0  14466  iswrddm0  14500  swrdnnn0nd  14619  swrdnd0  14620  swrdlsw  14630  pfxn0  14649  pfxnd0  14651  swrdswrdlem  14666  pfxccatin12lem3  14694  pfxccat3  14696  pfxccat3a  14700  swrdccat3blem  14701  cshwsublen  14758  cshwidxmod  14765  repswcshw  14774  cshw1  14784  trclun  14976  dmtrclfv  14980  rediv  15093  imdiv  15100  fsump1i  15731  modfsummods  15756  bpolydiflem  16019  bpoly3  16023  bpoly4  16024  cos1bnd  16154  sinltx  16156  rpnnen2lem1  16181  rpnnen2lem2  16182  rpnnen2lem12  16192  odd2np1  16310  opoe  16332  omoe  16333  opeo  16334  omeo  16335  gcdcllem1  16468  gcdaddmlem  16493  dfgcd2  16515  algfx  16549  lcmledvds  16568  lcmfunsnlem  16610  lcmfun  16614  coprmprod  16630  coprmproddvdslem  16631  odzval  16762  odzdvds  16766  prmreclem5  16891  mul4sq  16925  prmgaplem5  17026  prmgaplem6  17027  imasaddfnlem  17492  mreexexlem4d  17613  joindmss  18343  meetdmss  18357  gictr  19251  cntzval  19296  symg2bas  19368  odfval  19507  efgsfo  19714  efgrelexlemb  19725  dprddomcld  19978  dprdsubg  20001  dprd2da  20019  lssacs  20962  cnfldinv  21383  pzriprnglem7  21467  ocvval  21647  selvval  22101  dmatmul  22462  mdetfval1  22555  mndifsplit  22601  fvmptnn04if  22814  toprntopon  22890  opnnei  23085  ordtbas2  23156  ordtrest2lem  23168  lmmo  23345  fincmp  23358  bwth  23375  txbas  23532  ptcnplem  23586  tx2ndc  23616  hmphtr  23748  fbun  23805  filconn  23848  ptcmplem5  24021  cnextcn  24032  utoptop  24199  ucncn  24249  metust  24523  cfilucfil  24524  elcncf1di  24862  xrhmeo  24913  phtpycc  24958  copco  24985  pcohtpylem  24986  pcopt  24989  pcopt2  24990  ncvsi  25118  ovolval  25440  iunmbl2  25524  itg2splitlem  25715  cpnfval  25899  plyval  26158  fta1  26274  aaliou2b  26307  tayl0  26327  ulmdvlem3  26367  radcnvlem2  26379  dvradcnv  26386  reeff1o  26412  sincosq1lem  26461  sincosq2sgn  26463  sincosq4sgn  26465  sinq12ge0  26472  logrncl  26531  eflog  26540  cxpge0  26647  logb1  26733  atanf  26844  atanbnd  26890  igamf  27014  igamcl  27015  lgsne0  27298  mul2sq  27382  2sqreultblem  27411  pntibnd  27556  ostth  27602  nobdaymin  27745  nocvxminlem  27746  cutlt  27924  norec2ov  27949  addsuniflem  27993  mulsuniflem  28141  oldfib  28369  zmulscld  28389  zseo  28414  z12addscl  28469  mpteleeOLD  28964  axlowdimlem9  29019  axlowdimlem12  29022  axcontlem2  29034  axcontlem12  29044  structgrssvtx  29093  structgrssiedg  29094  lpvtx  29137  nbuhgr  29412  nbumgr  29416  nbuhgr2vtx1edgblem  29420  nbgr0edglem  29425  nbgr1vtx  29427  uvtx01vtx  29466  prcliscplgr  29483  cusgrsizeinds  29521  sizusglecusglem2  29531  uhgrvd00  29603  fusgrregdegfi  29638  rusgr1vtxlem  29656  wlkeq  29702  wlk1walk  29707  uspgr2wlkeq  29714  wlklenvclwlk  29722  wlkreslem  29736  wlkdlem2  29750  wlkdlem4  29752  spthonepeq  29820  cyclnumvtx  29868  clwlkclwwlkflem  30074  clwlkclwwlkfolem  30077  clwlkclwwlkf  30078  clwwisshclwws  30085  clwwlkneq0  30099  3wlkdlem6  30235  eupth2eucrct  30287  eupth2lem1  30288  eupth2lem3lem7  30304  frgr3vlem1  30343  frgr3vlem2  30344  frgrncvvdeqlem8  30376  frgrncvvdeqlem9  30377  numclwwlk5  30458  frgrreg  30464  frgrregord013  30465  friendshipgt3  30468  isgrpo  30568  vciOLD  30632  vcex  30649  nmogtmnf  30841  siilem1  30922  siii  30924  ajmoi  30929  bcsiALT  31250  hhcms  31274  ocval  31351  hsupval  31405  omlsilem  31473  h1de2bi  31625  h1de2ctlem  31626  hosubeq0i  31897  adjmo  31903  nmopgtmnf  31939  nlfnval  31952  nmcopex  32100  nmcfnex  32124  riesz4i  32134  riesz1  32136  riesz2  32137  opsqrlem1  32211  superpos  32425  hatomistici  32433  chpssati  32434  mdsymlem3  32476  3o1cs  32530  3o2cs  32531  3o3cs  32532  iunrnmptss  32635  brabgaf  32679  f1mptrn  32708  ffsrn  32801  xnn0gt0  32842  hashxpe  32880  sgn3da  32907  elrgspnlem4  33306  prmidl2  33501  mxidlnzrb  33540  evl1deg2  33637  evl1deg3  33638  fedgmul  33775  cos9thpiminplylem2  33927  ordtrest2NEWlem  34066  qqhval2  34126  esumfsup  34214  esumcvg  34230  cntnevol  34372  ddemeas  34380  dya2icoseg2  34422  dya2iocnei  34426  eulerpartlems  34504  eulerpartlemgvv  34520  eulerpart  34526  cndprobprob  34582  ballotlemsdom  34656  ballotth  34682  bnj945  34916  bnj1379  34972  bnj1459  34985  bnj557  35043  bnj571  35048  bnj849  35067  bnj964  35085  bnj978  35091  bnj1018g  35105  bnj1018  35106  bnj1020  35107  bnj1033  35111  bnj1175  35146  bnj1398  35176  bnj1417  35183  bnj1523  35213  nummin  35236  r1omhf  35249  axprALT2  35253  fineqvnttrclselem1  35265  onvf1odlem4  35288  onvf1od  35289  cusgr3cyclex  35318  txpconn  35414  satfv1  35545  satffun  35591  msubco  35713  mclsax  35751  dfon2lem7  35969  dfon2lem8  35970  pprodss4v  36064  fullfunfv  36129  altxpsspw  36159  funtransport  36213  fvtransport  36214  funray  36322  fvray  36323  funline  36324  fvline  36326  finminlem  36500  bisym1  36601  onsucconni  36619  onsucsuccmpi  36625  weiunse  36650  bj-currypara  36824  bj-cbvaw  36935  axc11n11r  36980  bj-equsal2  37132  bj-xpima1snALT  37264  bj-unexg  37345  bj-bm1.3ii  37371  bj-axseprep  37381  bj-axreprepsep  37382  bj-opelidb1ALT  37480  mptsnunlem  37654  iooelexlt  37678  relowlpssretop  37680  rdgeqoa  37686  difunieq  37690  nlpineqsn  37724  fvineqsneq  37728  wl-ax12v2cl  37822  wl-lem-nexmo  37892  matunitlindflem1  37937  ptrecube  37941  poimirlem26  37967  poimirlem30  37971  poimir  37974  ismblfin  37982  itg2addnclem  37992  dvasin  38025  sdclem2  38063  totbndbnd  38110  ismgmOLD  38171  exidresid  38200  isrngo  38218  rngoablo2  38230  rngoueqz  38261  isdivrngo  38271  isdrngo1  38277  isdrngo2  38279  ispridl2  38359  relcnveq3  38648  elrelscnveq3  38948  disjimeceqim  39125  dmqsblocks  39288  ax12eq  39387  ax12el  39388  lkr0f  39540  hl2at  39851  dalemswapyz  40102  pclfinclN  40396  osumcllem11N  40412  pexmidlem8N  40423  ltrnnid  40582  aks4d1p8  42526  redvmptabs  42792  sn-00id  42833  rictr  42965  eu6w  43109  mptfcl  43152  fphpd  43244  elmnc  43564  itgoval  43589  arearect  43643  reabsifpos  44061  clsk3nimkb  44467  grumnud  44713  nanorxor  44732  pm11.71  44824  iotavalsb  44860  sbiota1  44861  2uasbanh  44988  eel0TT  45130  eelT00  45131  eelTTT  45132  eelT11  45133  eelT12  45135  eelTT1  45136  eelT01  45137  eel0T1  45138  eelTT  45197  uunT1p1  45207  uun121  45209  uun121p1  45210  un2122  45216  uunTT1  45219  uunTT1p1  45220  uunTT1p2  45221  uunT11  45222  uunT11p1  45223  uunT11p2  45224  uunT12  45225  uunT12p1  45226  uunT12p2  45227  uunT12p3  45228  uunT12p4  45229  uunT12p5  45230  uun111  45231  3anidm12p2  45233  uun123  45234  3impdirp1  45242  undif3VD  45308  ax6e2ndeqVD  45335  2uasbanhVD  45337  ax6e2ndeqALT  45357  iunconnlem2  45361  sineq0ALT  45363  modelaxreplem1  45405  permaxrep  45433  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem3  46431  stoweidlem17  46445  fourierdlem42  46577  fourierdlem48  46582  fourierdlem50  46584  fourierdlem51  46585  fourierdlem76  46610  fourierdlem83  46617  fourierdlem87  46621  hoidmvval0  47015  evenwodadd  47317  rexrsb  47548  2reu8i  47561  2reuimp  47563  afv0nbfvbi  47599  afvfv0bi  47600  afveu  47601  fnbrafvb  47602  afvres  47620  tz6.12-afv  47621  dmfcoafv  47623  afvco2  47624  aovprc  47636  aovrcl  47637  aovmpt4g  47649  afv2eu  47686  afv2res  47687  tz6.12-afv2  47688  tz6.12i-afv2  47691  afv2rnfveq  47710  fvmptrab  47740  fvmptrabdm  47741  fzopred  47771  2ffzoeq  47776  muldvdsfacm1  47835  elsprel  47935  prproropf1o  47967  reupr  47982  lighneal  48074  odd2prm2  48194  even3prm2  48195  grictr  48399  grlimgrtrilem2  48478  usgrexmpl12ngric  48514  gpgprismgr4cycllem8  48578  gpgprismgr4cycllem11  48581  pgnbgreunbgrlem2lem1  48590  upgrwlkupwlk  48616  ovn0ssdmfun  48635  islinindfis  48925  rrx2linest  49218  line2ylem  49227  mofeu  49323  homf0  49484  uobffth  49693  uobeqw  49694  initopropd  49718  termopropd  49719  zeroopropd  49720  fucofvalne  49800  isthincd2  49912  lanrcl  50096  ranrcl  50097  setrec2fun  50167  elsetrecslem  50174  setrecsres  50177  secval  50222  cscval  50223  cotval  50224