Theorem sylbir 238

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 231	. 2 ⊢ (𝜑 → 𝜓)
3		sylbir.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 18	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3i  294  ex  417  3expa  1136  3ori  1451  an42ds  1520  nanass  1540  19.38  1869  19.35  1907  19.8aw  2082  sbrimvw  2125  equsexv  2304  sbi2  2337  nfeqf2  2409  equsex  2450  dfmoeu  2563  2mo  2676  axie2  2730  necon1bi  2986  necon1i  2991  r19.35  3123  spc2ed  3560  reu6  3689  rabssrabd  4037  uneqin  4242  difin0ss  4328  inelcm  4425  falseral0OLD  4476  raaan2  4483  difprsn1  4768  tppreqb  4773  n0snor2el  4798  unissint  4937  intminss  4939  dfiun2g  4994  iununi  5065  triin  5235  bm1.3iiOLD  5265  eusv2nf  5366  reusv3i  5375  axprglem  5407  axprg  5408  moabexOLD  5440  opelopabt  5516  eqrelrel  5783  opeliunxp2  5824  opelrn  5933  ssxpb  6172  xpima  6180  xpimasn  6183  dmsn0el  6212  relcnvtr  6269  relcoi2  6278  elsnxp  6292  reuop  6294  iotanul  6516  dffv2  6976  fnfvrnss  7116  fressnfv  7157  fconst5  7204  f1mpt  7259  isocnv3  7330  f1owe  7351  ovprc  7448  fvmpopr2d  7572  onminesb  7788  onminsb  7789  onintrab  7791  onnminsb  7794  ordsuci  7803  onsucuni2  7826  tfindsg2  7854  zfrep6OLD  7948  fo1stres  8008  fo2ndres  8009  bropopvvv  8081  bropfvvvv  8083  frxp  8118  poseq  8150  soseq  8151  opeliunxp2f  8202  mpoxopoveqd  8213  reldmtpos  8226  frrlem4  8282  tfrlem5  8362  tfrlem9  8368  tfr2  8381  rdgsuc  8407  oaordi  8527  oeordi  8569  omopthi  8643  on2recsov  8650  fvmptmap  8875  mptelixpg  8929  ener  8994  domtr  9000  unen  9038  undom  9049  dom0  9089  xpf1o  9123  mapen  9125  pssnn  9149  unfi  9151  ssfi  9153  ensymfib  9164  entrfil  9165  enfii  9166  domtrfil  9172  unxpdomlem3  9214  isinf  9221  frfi  9241  unblem1  9248  fofinf1o  9285  fsuppun  9343  elirrvOLD  9556  inf3lem2  9594  inf3lem5  9597  cantnfp1lem1  9643  cantnfp1lem3  9645  tcmin  9704  setinds  9714  frr2  9728  r1ordg  9746  r1ord  9748  rankr1ai  9766  r1val3  9806  bndrank  9809  unbndrank  9810  rankr1b  9832  rankxplim3  9849  tcrank  9852  xpnum  9933  cardmin2  9981  infxpenlem  9993  fseqen  10007  dfac8clem  10012  alephsson  10080  alephfp  10088  dfac4  10102  kmlem6  10135  kmlem8  10137  kmlem9  10138  cflem  10224  infpssr  10287  fin1a2lem12  10390  axcc4  10418  axcc4dom  10420  ac6s2  10465  zornn0g  10484  cardidg  10527  unsnen  10532  pwcfsdom  10563  cfpwsdom  10564  gchpwdom  10650  r1tskina  10762  intgru  10794  indpi  10887  nqereu  10909  supsrlem  11091  letrii  11330  dfnn3  12242  zaddcl  12629  nn0ind  12686  fnn0ind  12690  ublbneg  12952  nn01to3  12960  infmrp1  13366  fz0  13562  fzo1fzo0n0  13740  elfzom1elp1fzo  13757  fzo0end  13783  elfznelfzo  13798  fzind2  13813  injresinjlem  13815  fleqceilz  13883  nnsinds  14020  nn0sinds  14021  faclbnd4lem1  14325  hashinf  14367  hasheqf1oi  14383  hashgt0elex  14433  hashgt23el  14457  hashfacen  14487  hash2prde  14503  hash2sspr  14522  fun2dmnop0  14537  iswrddm0  14571  swrdnnn0nd  14690  swrdnd0  14691  swrdlsw  14701  pfxn0  14720  pfxnd0  14722  swrdswrdlem  14737  pfxccatin12lem3  14765  pfxccat3  14767  pfxccat3a  14771  swrdccat3blem  14772  cshwsublen  14829  cshwidxmod  14836  repswcshw  14845  cshw1  14855  trclun  15047  dmtrclfv  15051  sgn3da  15134  rediv  15178  imdiv  15185  fsump1i  15816  modfsummods  15841  bpolydiflem  16103  bpoly3  16107  bpoly4  16108  cos1bnd  16238  sinltx  16240  rpnnen2lem1  16265  rpnnen2lem2  16266  rpnnen2lem12  16276  odd2np1  16394  opoe  16416  omoe  16417  opeo  16418  omeo  16419  gcdcllem1  16552  gcdaddmlem  16577  dfgcd2  16599  algfx  16633  lcmledvds  16652  lcmfunsnlem  16694  lcmfun  16698  coprmprod  16714  coprmproddvdslem  16715  odzval  16846  odzdvds  16850  prmreclem5  16975  mul4sq  17009  prmgaplem5  17110  prmgaplem6  17111  imasaddfnlem  17577  mreexexlem4d  17698  joindmss  18428  meetdmss  18442  gictr  19341  cntzval  19386  symg2bas  19458  odfval  19597  efgsfo  19804  efgrelexlemb  19815  dprddomcld  20068  dprdsubg  20091  dprd2da  20109  rictr  20600  isdrng3lem1  20851  isdrng3  20853  lssacs  21088  prmidl2  21466  cnfldinv  21553  pzriprnglem7  21637  ocvval  21817  selvval  22271  dmatmul  22654  mdetfval1  22747  mndifsplit  22793  fvmptnn04if  23006  toprntopon  23082  opnnei  23277  ordtbas2  23348  ordtrest2lem  23360  lmmo  23537  fincmp  23550  bwth  23567  txbas  23724  ptcnplem  23778  tx2ndc  23808  hmphtr  23940  fbun  23997  filconn  24040  ptcmplem5  24213  cnextcn  24224  utoptop  24391  ucncn  24441  metust  24715  cfilucfil  24716  elcncf1di  25054  xrhmeo  25105  phtpycc  25150  copco  25177  pcohtpylem  25178  pcopt  25181  pcopt2  25182  ncvsi  25310  ovolval  25632  iunmbl2  25716  itg2splitlem  25907  cpnfval  26091  plyval  26350  fta1  26469  aaliou2b  26504  tayl0  26525  ulmdvlem3  26565  radcnvlem2  26577  dvradcnv  26584  reeff1o  26610  sincosq1lem  26662  sincosq2sgn  26664  sincosq4sgn  26666  sinq12ge0  26673  logrncl  26732  eflog  26741  cxpge0  26848  logb1  26934  atanf  27045  atanbnd  27091  igamf  27215  igamcl  27216  lgsne0  27499  mul2sq  27583  2sqreultblem  27612  pntibnd  27757  ostth  27803  nobdaymin  27946  nocvxminlem  27947  cutlt  28125  norec2ov  28150  addsuniflem  28194  mulsuniflem  28342  oldfib  28570  zmulscld  28590  zseo  28615  z12addscl  28670  mpteleeOLD  29245  axlowdimlem9  29300  axlowdimlem12  29303  axcontlem2  29315  axcontlem12  29325  structgrssvtx  29374  structgrssiedg  29375  lpvtx  29418  nbuhgr  29693  nbumgr  29697  nbuhgr2vtx1edgblem  29701  nbgr0edglem  29706  nbgr1vtx  29708  uvtx01vtx  29747  prcliscplgr  29764  cusgrsizeinds  29802  sizusglecusglem2  29812  uhgrvd00  29884  fusgrregdegfi  29919  rusgr1vtxlem  29937  wlkeq  29983  wlk1walk  29988  uspgr2wlkeq  29995  wlklenvclwlk  30003  wlkreslem  30017  wlkdlem2  30031  wlkdlem4  30033  spthonepeq  30101  cyclnumvtx  30149  clwlkclwwlkflem  30355  clwlkclwwlkfolem  30358  clwlkclwwlkf  30359  clwwisshclwws  30366  clwwlkneq0  30380  3wlkdlem6  30516  eupth2eucrct  30568  eupth2lem1  30569  eupth2lem3lem7  30585  frgr3vlem1  30624  frgr3vlem2  30625  frgrncvvdeqlem8  30657  frgrncvvdeqlem9  30658  numclwwlk5  30739  frgrreg  30745  frgrregord013  30746  friendshipgt3  30749  isgrpo  30849  vciOLD  30913  vcex  30930  nmogtmnf  31122  siilem1  31203  siii  31205  ajmoi  31210  bcsiALT  31531  hhcms  31555  ocval  31632  hsupval  31686  omlsilem  31754  h1de2bi  31906  h1de2ctlem  31907  hosubeq0i  32178  adjmo  32184  nmopgtmnf  32220  nlfnval  32233  nmcopex  32381  nmcfnex  32405  riesz4i  32415  riesz1  32417  riesz2  32418  opsqrlem1  32492  superpos  32706  hatomistici  32714  chpssati  32715  mdsymlem3  32757  3o1cs  32809  3o2cs  32810  3o3cs  32811  iunrnmptss  32910  brabgaf  32951  f1mptrn  32980  ffsrn  33073  xnn0gt0  33114  hashxpe  33152  elrgspnlem4  33565  mxidlnzrb  33762  evl1deg2  33867  evl1deg3  33868  fedgmul  34021  cos9thpiminplylem2  34173  ordtrest2NEWlem  34312  qqhval2  34372  esumfsup  34460  esumcvg  34476  cntnevol  34618  ddemeas  34626  dya2icoseg2  34668  dya2iocnei  34672  eulerpartlems  34750  eulerpartlemgvv  34766  eulerpart  34772  cndprobprob  34828  ballotlemsdom  34902  ballotth  34928  bnj945  35162  bnj1379  35218  bnj1459  35231  bnj557  35289  bnj571  35294  bnj849  35313  bnj964  35331  bnj978  35337  bnj1018g  35351  bnj1018  35352  bnj1020  35353  bnj1033  35357  bnj1175  35392  bnj1398  35422  bnj1417  35429  bnj1523  35459  nummin  35484  r1omhf  35500  axprALT2  35503  fineqvnttrclselem1  35534  rankkardu  35584  onvf1odlem4  35590  onvf1od  35591  vonf1osev  35596  vonf1oonfo  35599  cusgr3cyclex  35628  txpconn  35724  satfv1  35855  satffun  35901  msubco  36023  mclsax  36061  dfon2lem7  36279  dfon2lem8  36280  pprodss4v  36374  fullfunfv  36439  altxpsspw  36469  funtransport  36523  fvtransport  36524  funray  36632  fvray  36633  funline  36634  fvline  36636  finminlem  36849  bisym1  36950  onsucconni  36968  onsucsuccmpi  36974  weiunse  36999  bj-currypara  37172  bj-cbvaw  37283  axc11n11r  37328  bj-equsal2  37480  bj-xpima1snALT  37613  bj-unexg  37694  bj-bm1.3ii  37720  bj-axseprep  37731  bj-axreprepsep  37732  bj-opelidb1ALT  37830  mptsnunlem  38004  iooelexlt  38028  relowlpssretop  38030  rdgeqoa  38036  difunieq  38040  nlpineqsn  38074  fvineqsneq  38078  wl-ax12v2cl  38172  wl-lem-nexmo  38242  matunitlindflem1  38287  ptrecube  38291  poimirlem26  38317  poimirlem30  38321  poimir  38324  ismblfin  38332  itg2addnclem  38342  dvasin  38375  sdclem2  38413  totbndbnd  38460  ismgmOLD  38521  exidresid  38550  isrngo  38568  rngoablo2  38580  rngoueqz  38611  isdivrngo  38621  isdrngo1  38627  isdrngo2  38629  ispridl2  38709  relcnveq3  38996  elrelscnveq3  39296  disjimeceqim  39473  dmqsblocks  39636  ax12eq  39735  ax12el  39736  lkr0f  39888  hl2at  40199  dalemswapyz  40450  pclfinclN  40744  osumcllem11N  40760  pexmidlem8N  40771  ltrnnid  40930  aks4d1p8  42874  redvmptabs  43141  sn-00id  43182  eu6w  43428  mptfcl  43471  fphpd  43563  elmnc  43883  itgoval  43908  arearect  43962  reabsifpos  44380  clsk3nimkb  44786  grumnud  45016  nanorxor  45035  pm11.71  45127  iotavalsb  45163  sbiota1  45164  2uasbanh  45290  eel0TT  45432  eelT00  45433  eelTTT  45434  eelT11  45435  eelT12  45437  eelTT1  45438  eelT01  45439  eel0T1  45440  eelTT  45499  uunT1p1  45509  uun121  45511  uun121p1  45512  un2122  45518  uunTT1  45521  uunTT1p1  45522  uunTT1p2  45523  uunT11  45524  uunT11p1  45525  uunT11p2  45526  uunT12  45527  uunT12p1  45528  uunT12p2  45529  uunT12p3  45530  uunT12p4  45531  uunT12p5  45532  uun111  45533  3anidm12p2  45535  uun123  45536  3impdirp1  45544  undif3VD  45610  ax6e2ndeqVD  45637  2uasbanhVD  45639  ax6e2ndeqALT  45659  iunconnlem2  45663  sineq0ALT  45665  modelaxreplem1  45707  permaxrep  45735  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  stoweidlem3  46737  stoweidlem17  46751  fourierdlem42  46883  fourierdlem48  46888  fourierdlem50  46890  fourierdlem51  46891  fourierdlem76  46916  fourierdlem83  46923  fourierdlem87  46927  hoidmvval0  47321  evenwodadd  47622  rexrsb  47857  2reu8i  47870  2reuimp  47872  afv0nbfvbi  47908  afvfv0bi  47909  afveu  47910  fnbrafvb  47911  afvres  47929  tz6.12-afv  47930  dmfcoafv  47932  afvco2  47933  aovprc  47945  aovrcl  47946  aovmpt4g  47958  afv2eu  47995  afv2res  47996  tz6.12-afv2  47997  tz6.12i-afv2  48000  afv2rnfveq  48019  fvmptrab  48049  fvmptrabdm  48050  fzopred  48080  2ffzoeq  48085  muldvdsfacm1  48144  elsprel  48244  prproropf1o  48276  reupr  48291  lighneal  48383  odd2prm2  48503  even3prm2  48504  grictr  48708  grlimgrtrilem2  48787  usgrexmpl12ngric  48823  gpgprismgr4cycllem8  48887  gpgprismgr4cycllem11  48890  pgnbgreunbgrlem2lem1  48899  upgrwlkupwlk  48925  ovn0ssdmfun  48944  islinindfis  49249  rrx2linest  49542  line2ylem  49551  mofeu  49646  homf0  49807  uobffth  50016  uobeqw  50017  initopropd  50041  termopropd  50042  zeroopropd  50043  fucofvalne  50123  isthincd2  50235  lanrcl  50419  ranrcl  50420  setrec2fun  50490  elsetrecslem  50497  setrecsres  50500  secval  50545  cscval  50546  cotval  50547