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  1118  3ori  1426  nanass  1510  19.38  1839  19.35  1877  19.8aw  2050  equsexv  2268  sbi2  2302  nfeqf2  2381  equsex  2422  dfmoeu  2535  2mo  2647  axie2  2702  necon1bi  2960  necon1i  2965  r19.35  3095  r19.35OLD  3096  sbhypfOLD  3524  spc2ed  3580  reu6  3709  rabssrabd  4058  uneqin  4264  difin0ss  4348  inelcm  4440  rzal  4484  ralf0  4489  falseral0  4491  raaan2  4496  difprsn1  4776  tppreqb  4781  n0snor2el  4809  unissint  4948  intminss  4950  dfiun2g  5006  iununi  5075  triin  5246  bm1.3iiOLD  5272  eusv2nf  5365  reusv3i  5374  moabex  5434  opelopabt  5507  eqrelrel  5776  opeliunxp2  5818  opelrn  5923  ssxpb  6163  xpima  6171  xpimasn  6174  dmsn0el  6200  relcnvtr  6256  relcoi2  6266  elsnxp  6280  reuop  6282  iotanul  6508  f1imadifssran  6621  dffv2  6973  fnfvrnss  7110  fressnfv  7149  fconst5  7197  f1mpt  7253  isocnv3  7324  f1owe  7345  ovprc  7441  fvmpopr2d  7567  onminesb  7785  onminsb  7786  onintrab  7788  onnminsb  7791  ordsuci  7800  onsucuni2  7826  tfindsg2  7855  zfrep6  7951  fo1stres  8012  fo2ndres  8013  bropopvvv  8087  bropfvvvv  8089  frxp  8123  poseq  8155  soseq  8156  opeliunxp2f  8207  mpoxopoveqd  8218  reldmtpos  8231  frrlem4  8286  wfrlem4OLD  8324  wfrlem12OLD  8332  wfrlem16OLD  8336  wfr2OLD  8340  tfrlem5  8392  tfrlem9  8397  tfr2  8410  rdgsuc  8436  oaordi  8556  oeordi  8597  omopthi  8671  on2recsov  8678  fvmptmap  8893  mptelixpg  8947  ener  9013  domtr  9019  snfiOLD  9056  unen  9058  undom  9071  dom0  9114  xpf1o  9151  mapen  9153  rexdif1enOLD  9171  dif1enOLD  9174  pssnn  9180  unfi  9183  ssfi  9185  ensymfib  9196  entrfil  9197  enfii  9198  domtrfil  9204  unxpdomlem3  9258  isinf  9266  isinfOLD  9267  frfi  9291  unblem1  9298  fofinf1o  9342  fsuppun  9397  inf3lem2  9641  inf3lem5  9644  cantnfp1lem1  9690  cantnfp1lem3  9692  tcmin  9753  frr2  9772  r1ordg  9790  r1ord  9792  rankr1ai  9810  r1val3  9850  bndrank  9853  unbndrank  9854  rankr1b  9876  rankxplim3  9893  tcrank  9896  xpnum  9963  cardmin2  10011  infxpenlem  10025  fseqen  10039  dfac8clem  10044  alephsson  10112  alephfp  10120  dfac4  10134  kmlem6  10168  kmlem8  10170  kmlem9  10171  cflem  10257  infpssr  10320  fin1a2lem12  10423  axcc4  10451  axcc4dom  10453  ac6s2  10498  zornn0g  10517  cardidg  10560  unsnen  10565  pwcfsdom  10595  cfpwsdom  10596  gchpwdom  10682  r1tskina  10794  intgru  10826  indpi  10919  nqereu  10941  supsrlem  11123  letrii  11358  dfnn3  12252  zaddcl  12630  nn0ind  12686  fnn0ind  12690  ublbneg  12947  nn01to3  12955  infmrp1  13359  fz0  13554  fzo1fzo0n0  13729  elfzom1elp1fzo  13746  fzo0end  13772  elfznelfzo  13786  fzind2  13799  injresinjlem  13801  fleqceilz  13869  nnsinds  14004  nn0sinds  14005  faclbnd4lem1  14309  hashinf  14351  hasheqf1oi  14367  hashgt0elex  14417  hashgt23el  14440  hashfacen  14470  hash2prde  14486  hash2sspr  14505  fun2dmnop0  14520  iswrddm0  14554  swrdnnn0nd  14672  swrdnd0  14673  swrdlsw  14683  pfxn0  14702  pfxnd0  14704  swrdswrdlem  14720  pfxccatin12lem3  14748  pfxccat3  14750  pfxccat3a  14754  swrdccat3blem  14755  cshwsublen  14812  cshwidxmod  14819  repswcshw  14828  cshw1  14838  trclun  15031  dmtrclfv  15035  rediv  15148  imdiv  15155  fsump1i  15783  modfsummods  15807  bpolydiflem  16068  bpoly3  16072  bpoly4  16073  cos1bnd  16203  sinltx  16205  rpnnen2lem1  16230  rpnnen2lem2  16231  rpnnen2lem12  16241  odd2np1  16358  opoe  16380  omoe  16381  opeo  16382  omeo  16383  gcdcllem1  16516  gcdaddmlem  16541  dfgcd2  16563  algfx  16597  lcmledvds  16616  lcmfunsnlem  16658  lcmfun  16662  coprmprod  16678  coprmproddvdslem  16679  odzval  16809  odzdvds  16813  prmreclem5  16938  mul4sq  16972  prmgaplem5  17073  prmgaplem6  17074  imasaddfnlem  17540  mreexexlem4d  17657  joindmss  18387  meetdmss  18401  gictr  19257  cntzval  19302  symg2bas  19372  odfval  19511  efgsfo  19718  efgrelexlemb  19729  dprddomcld  19982  dprdsubg  20005  dprd2da  20023  lssacs  20922  cnfldinv  21363  pzriprnglem7  21446  ocvval  21625  selvval  22071  dmatmul  22433  mdetfval1  22526  mndifsplit  22572  fvmptnn04if  22785  toprntopon  22861  opnnei  23056  ordtbas2  23127  ordtrest2lem  23139  lmmo  23316  fincmp  23329  bwth  23346  txbas  23503  ptcnplem  23557  tx2ndc  23587  hmphtr  23719  fbun  23776  filconn  23819  ptcmplem5  23992  cnextcn  24003  utoptop  24171  ucncn  24221  metust  24495  cfilucfil  24496  elcncf1di  24837  xrhmeo  24893  phtpycc  24939  copco  24967  pcohtpylem  24968  pcopt  24971  pcopt2  24972  ncvsi  25101  ovolval  25424  iunmbl2  25508  itg2splitlem  25699  cpnfval  25884  plyval  26148  fta1  26266  aaliou2b  26299  tayl0  26319  ulmdvlem3  26361  radcnvlem2  26373  dvradcnv  26380  reeff1o  26407  sincosq1lem  26456  sincosq2sgn  26458  sincosq4sgn  26460  sinq12ge0  26467  logrncl  26526  eflog  26535  cxpge0  26642  logb1  26729  atanf  26840  atanbnd  26886  igamf  27011  igamcl  27012  lgsne0  27296  mul2sq  27380  2sqreultblem  27409  pntibnd  27554  ostth  27600  nocvxminlem  27739  nocvxmin  27740  cutlt  27883  norec2ov  27907  addsuniflem  27951  mulsuniflem  28092  zmulscld  28300  zseo  28323  mptelee  28820  axlowdimlem9  28875  axlowdimlem12  28878  axcontlem2  28890  axcontlem12  28900  structgrssvtx  28949  structgrssiedg  28950  lpvtx  28993  nbuhgr  29268  nbumgr  29272  nbuhgr2vtx1edgblem  29276  nbgr0edglem  29281  nbgr1vtx  29283  uvtx01vtx  29322  prcliscplgr  29339  cusgrsizeinds  29378  sizusglecusglem2  29388  uhgrvd00  29460  fusgrregdegfi  29495  rusgr1vtxlem  29513  wlkeq  29560  wlk1walk  29565  uspgr2wlkeq  29572  wlklenvclwlk  29581  wlkreslem  29595  wlkdlem2  29609  wlkdlem4  29611  spthonepeq  29680  cyclnumvtx  29728  clwlkclwwlkflem  29931  clwlkclwwlkfolem  29934  clwlkclwwlkf  29935  clwwisshclwws  29942  clwwlkneq0  29956  3wlkdlem6  30092  eupth2eucrct  30144  eupth2lem1  30145  eupth2lem3lem7  30161  frgr3vlem1  30200  frgr3vlem2  30201  frgrncvvdeqlem8  30233  frgrncvvdeqlem9  30234  numclwwlk5  30315  frgrreg  30321  frgrregord013  30322  friendshipgt3  30325  isgrpo  30424  vciOLD  30488  vcex  30505  nmogtmnf  30697  siilem1  30778  siii  30780  ajmoi  30785  bcsiALT  31106  hhcms  31130  ocval  31207  hsupval  31261  omlsilem  31329  h1de2bi  31481  h1de2ctlem  31482  hosubeq0i  31753  adjmo  31759  nmopgtmnf  31795  nlfnval  31808  nmcopex  31956  nmcfnex  31980  riesz4i  31990  riesz1  31992  riesz2  31993  opsqrlem1  32067  superpos  32281  hatomistici  32289  chpssati  32290  mdsymlem3  32332  an42ds  32377  3o1cs  32388  3o2cs  32389  3o3cs  32390  iunrnmptss  32492  brabgaf  32534  f1mptrn  32559  ffsrn  32652  fpwrelmap  32656  xnn0gt0  32692  hashxpe  32732  sgn3da  32759  elrgspnlem4  33186  prmidl2  33402  mxidlnzrb  33441  evl1deg2  33536  evl1deg3  33537  fedgmul  33617  cos9thpiminplylem2  33763  ordtrest2NEWlem  33899  qqhval2  33959  esumfsup  34047  esumcvg  34063  cntnevol  34205  ddemeas  34213  dya2icoseg2  34256  dya2iocnei  34260  eulerpartlems  34338  eulerpartlemgvv  34354  eulerpart  34360  cndprobprob  34416  ballotlemsdom  34490  ballotth  34516  bnj945  34750  bnj1379  34807  bnj1459  34820  bnj557  34878  bnj571  34883  bnj849  34902  bnj964  34920  bnj978  34926  bnj1018g  34940  bnj1018  34941  bnj1020  34942  bnj1033  34946  bnj1175  34981  bnj1398  35011  bnj1417  35018  bnj1523  35048  nummin  35068  cusgr3cyclex  35104  txpconn  35200  satfv1  35331  satffun  35377  msubco  35499  mclsax  35537  setinds  35742  dfon2lem7  35753  dfon2lem8  35754  pprodss4v  35848  fullfunfv  35911  altxpsspw  35941  funtransport  35995  fvtransport  35996  funray  36104  fvray  36105  funline  36106  fvline  36108  finminlem  36282  bisym1  36383  onsucconni  36401  onsucsuccmpi  36407  weiunse  36432  bj-currypara  36524  axc11n11r  36647  bj-equsal2  36789  bj-xpima1snALT  36921  bj-unexg  37002  bj-bm1.3ii  37028  bj-opelidb1ALT  37130  mptsnunlem  37302  iooelexlt  37326  relowlpssretop  37328  rdgeqoa  37334  difunieq  37338  nlpineqsn  37372  fvineqsneq  37376  wl-ax12v2cl  37470  wl-lem-nexmo  37531  matunitlindflem1  37586  ptrecube  37590  poimirlem26  37616  poimirlem30  37620  poimir  37623  ismblfin  37631  itg2addnclem  37641  dvasin  37674  sdclem2  37712  totbndbnd  37759  ismgmOLD  37820  exidresid  37849  isrngo  37867  rngoablo2  37879  rngoueqz  37910  isdivrngo  37920  isdrngo1  37926  isdrngo2  37928  ispridl2  38008  relcnveq3  38285  elrelscnveq3  38455  ax12eq  38905  ax12el  38906  lkr0f  39058  hl2at  39370  dalemswapyz  39621  pclfinclN  39915  osumcllem11N  39931  pexmidlem8N  39942  ltrnnid  40101  aks4d1p8  42046  redvmptabs  42350  sn-00id  42391  rictr  42490  eu6w  42646  mptfcl  42690  fphpd  42786  elmnc  43107  itgoval  43132  arearect  43186  reabsifpos  43605  clsk3nimkb  44011  grumnud  44258  nanorxor  44277  pm11.71  44369  iotavalsb  44405  sbiota1  44406  2uasbanh  44534  eel0TT  44676  eelT00  44677  eelTTT  44678  eelT11  44679  eelT12  44681  eelTT1  44682  eelT01  44683  eel0T1  44684  eelTT  44743  uunT1p1  44753  uun121  44755  uun121p1  44756  un2122  44762  uunTT1  44765  uunTT1p1  44766  uunTT1p2  44767  uunT11  44768  uunT11p1  44769  uunT11p2  44770  uunT12  44771  uunT12p1  44772  uunT12p2  44773  uunT12p3  44774  uunT12p4  44775  uunT12p5  44776  uun111  44777  3anidm12p2  44779  uun123  44780  3impdirp1  44788  undif3VD  44854  ax6e2ndeqVD  44881  2uasbanhVD  44883  ax6e2ndeqALT  44903  iunconnlem2  44907  sineq0ALT  44909  modelaxreplem1  44951  permaxrep  44979  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  stoweidlem3  45980  stoweidlem17  45994  fourierdlem42  46126  fourierdlem48  46131  fourierdlem50  46133  fourierdlem51  46134  fourierdlem76  46159  fourierdlem83  46166  fourierdlem87  46170  hoidmvval0  46564  evenwodadd  46865  rexrsb  47077  2reu8i  47090  2reuimp  47092  afv0nbfvbi  47128  afvfv0bi  47129  afveu  47130  fnbrafvb  47131  afvres  47149  tz6.12-afv  47150  dmfcoafv  47152  afvco2  47153  aovprc  47165  aovrcl  47166  aovmpt4g  47178  afv2eu  47215  afv2res  47216  tz6.12-afv2  47217  tz6.12i-afv2  47220  afv2rnfveq  47239  fvmptrab  47269  fvmptrabdm  47270  fzopred  47299  2ffzoeq  47304  elsprel  47437  prproropf1o  47469  reupr  47484  lighneal  47573  odd2prm2  47680  even3prm2  47681  grictr  47884  grlimgrtrilem2  47955  usgrexmpl12ngric  47990  gpgprismgr4cycllem8  48049  gpgprismgr4cycllem11  48052  upgrwlkupwlk  48063  ovn0ssdmfun  48082  islinindfis  48373  rrx2linest  48670  line2ylem  48679  mofeu  48774  homf0  48932  initopropd  49108  termopropd  49109  zeroopropd  49110  fucofvalne  49184  isthincd2  49271  lanrcl  49444  ranrcl  49445  setrec2fun  49504  elsetrecslem  49511  setrecsres  49514  secval  49559  cscval  49560  cotval  49561