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  1426  nanass  1510  19.38  1839  19.35  1877  19.8aw  2050  equsexv  2268  sbi2  2302  nfeqf2  2382  equsex  2423  dfmoeu  2536  2mo  2648  axie2  2703  necon1bi  2969  necon1i  2974  r19.35  3108  r19.35OLD  3109  sbhypfOLD  3545  spc2ed  3601  reu6  3732  rabssrabd  4083  uneqin  4289  difin0ss  4373  inelcm  4465  rzal  4509  ralf0  4514  falseral0  4516  raaan2  4521  difprsn1  4800  tppreqb  4805  n0snor2el  4833  unissint  4972  intminss  4974  dfiun2g  5030  iununi  5099  triin  5276  bm1.3iiOLD  5302  eusv2nf  5395  reusv3i  5404  moabex  5464  opelopabt  5537  eqrelrel  5807  opeliunxp2  5849  opelrn  5954  ssxpb  6194  xpima  6202  xpimasn  6205  dmsn0el  6231  relcnvtr  6287  relcoi2  6297  elsnxp  6311  reuop  6313  iotanul  6539  f1imadifssran  6652  dffv2  7004  fnfvrnss  7141  fressnfv  7180  fconst5  7226  f1mpt  7281  isocnv3  7352  f1owe  7373  ovprc  7469  fvmpopr2d  7595  onminesb  7813  onminsb  7814  onintrab  7816  onnminsb  7819  ordsuci  7828  onsucuni2  7854  tfindsg2  7883  zfrep6  7979  fo1stres  8040  fo2ndres  8041  bropopvvv  8115  bropfvvvv  8117  frxp  8151  poseq  8183  soseq  8184  opeliunxp2f  8235  mpoxopoveqd  8246  reldmtpos  8259  frrlem4  8314  wfrlem4OLD  8352  wfrlem12OLD  8360  wfrlem16OLD  8364  wfr2OLD  8368  tfrlem5  8420  tfrlem9  8425  tfr2  8438  rdgsuc  8464  oaordi  8584  oeordi  8625  omopthi  8699  on2recsov  8706  fvmptmap  8921  mptelixpg  8975  ener  9041  domtr  9047  snfiOLD  9084  unen  9086  undom  9099  dom0  9142  xpf1o  9179  mapen  9181  rexdif1enOLD  9199  dif1enOLD  9202  pssnn  9208  unfi  9211  ssfi  9213  ensymfib  9224  entrfil  9225  enfii  9226  domtrfil  9232  unxpdomlem3  9288  isinf  9296  isinfOLD  9297  frfi  9321  unblem1  9328  fofinf1o  9372  fsuppun  9427  inf3lem2  9669  inf3lem5  9672  cantnfp1lem1  9718  cantnfp1lem3  9720  tcmin  9781  frr2  9800  r1ordg  9818  r1ord  9820  rankr1ai  9838  r1val3  9878  bndrank  9881  unbndrank  9882  rankr1b  9904  rankxplim3  9921  tcrank  9924  xpnum  9991  cardmin2  10039  infxpenlem  10053  fseqen  10067  dfac8clem  10072  alephsson  10140  alephfp  10148  dfac4  10162  kmlem6  10196  kmlem8  10198  kmlem9  10199  cflem  10285  infpssr  10348  fin1a2lem12  10451  axcc4  10479  axcc4dom  10481  ac6s2  10526  zornn0g  10545  cardidg  10588  unsnen  10593  pwcfsdom  10623  cfpwsdom  10624  gchpwdom  10710  r1tskina  10822  intgru  10854  indpi  10947  nqereu  10969  supsrlem  11151  letrii  11386  dfnn3  12280  zaddcl  12657  nn0ind  12713  fnn0ind  12717  ublbneg  12975  nn01to3  12983  infmrp1  13386  fz0  13579  fzo1fzo0n0  13754  elfzom1elp1fzo  13771  fzo0end  13797  elfznelfzo  13811  fzind2  13824  injresinjlem  13826  fleqceilz  13894  nnsinds  14029  nn0sinds  14030  faclbnd4lem1  14332  hashinf  14374  hasheqf1oi  14390  hashgt0elex  14440  hashgt23el  14463  hashfacen  14493  hash2prde  14509  hash2sspr  14528  fun2dmnop0  14543  iswrddm0  14576  swrdnnn0nd  14694  swrdnd0  14695  swrdlsw  14705  pfxn0  14724  pfxnd0  14726  swrdswrdlem  14742  pfxccatin12lem3  14770  pfxccat3  14772  pfxccat3a  14776  swrdccat3blem  14777  cshwsublen  14834  cshwidxmod  14841  repswcshw  14850  cshw1  14860  trclun  15053  dmtrclfv  15057  rediv  15170  imdiv  15177  fsump1i  15805  modfsummods  15829  bpolydiflem  16090  bpoly3  16094  bpoly4  16095  cos1bnd  16223  sinltx  16225  rpnnen2lem1  16250  rpnnen2lem2  16251  rpnnen2lem12  16261  odd2np1  16378  opoe  16400  omoe  16401  opeo  16402  omeo  16403  gcdcllem1  16536  gcdaddmlem  16561  dfgcd2  16583  algfx  16617  lcmledvds  16636  lcmfunsnlem  16678  lcmfun  16682  coprmprod  16698  coprmproddvdslem  16699  odzval  16829  odzdvds  16833  prmreclem5  16958  mul4sq  16992  prmgaplem5  17093  prmgaplem6  17094  imasaddfnlem  17573  mreexexlem4d  17690  joindmss  18424  meetdmss  18438  gictr  19294  cntzval  19339  symg2bas  19410  odfval  19550  efgsfo  19757  efgrelexlemb  19768  dprddomcld  20021  dprdsubg  20044  dprd2da  20062  lssacs  20965  cnfldinv  21415  pzriprnglem7  21498  ocvval  21685  selvval  22139  dmatmul  22503  mdetfval1  22596  mndifsplit  22642  fvmptnn04if  22855  toprntopon  22931  opnnei  23128  ordtbas2  23199  ordtrest2lem  23211  lmmo  23388  fincmp  23401  bwth  23418  txbas  23575  ptcnplem  23629  tx2ndc  23659  hmphtr  23791  fbun  23848  filconn  23891  ptcmplem5  24064  cnextcn  24075  utoptop  24243  ucncn  24294  metust  24571  cfilucfil  24572  elcncf1di  24921  xrhmeo  24977  phtpycc  25023  copco  25051  pcohtpylem  25052  pcopt  25055  pcopt2  25056  ncvsi  25185  ovolval  25508  iunmbl2  25592  itg2splitlem  25783  cpnfval  25968  plyval  26232  fta1  26350  aaliou2b  26383  tayl0  26403  ulmdvlem3  26445  radcnvlem2  26457  dvradcnv  26464  reeff1o  26491  sincosq1lem  26539  sincosq2sgn  26541  sincosq4sgn  26543  sinq12ge0  26550  logrncl  26609  eflog  26618  cxpge0  26725  logb1  26812  atanf  26923  atanbnd  26969  igamf  27094  igamcl  27095  lgsne0  27379  mul2sq  27463  2sqreultblem  27492  pntibnd  27637  ostth  27683  nocvxminlem  27822  nocvxmin  27823  cutlt  27966  norec2ov  27990  addsuniflem  28034  mulsuniflem  28175  zmulscld  28383  zseo  28406  mptelee  28910  axlowdimlem9  28965  axlowdimlem12  28968  axcontlem2  28980  axcontlem12  28990  structgrssvtx  29041  structgrssiedg  29042  lpvtx  29085  nbuhgr  29360  nbumgr  29364  nbuhgr2vtx1edgblem  29368  nbgr0edglem  29373  nbgr1vtx  29375  uvtx01vtx  29414  prcliscplgr  29431  cusgrsizeinds  29470  sizusglecusglem2  29480  uhgrvd00  29552  fusgrregdegfi  29587  rusgr1vtxlem  29605  wlkeq  29652  wlk1walk  29657  uspgr2wlkeq  29664  wlklenvclwlk  29673  wlkreslem  29687  wlkdlem2  29701  wlkdlem4  29703  spthonepeq  29772  cyclnumvtx  29820  clwlkclwwlkflem  30023  clwlkclwwlkfolem  30026  clwlkclwwlkf  30027  clwwisshclwws  30034  clwwlkneq0  30048  3wlkdlem6  30184  eupth2eucrct  30236  eupth2lem1  30237  eupth2lem3lem7  30253  frgr3vlem1  30292  frgr3vlem2  30293  frgrncvvdeqlem8  30325  frgrncvvdeqlem9  30326  numclwwlk5  30407  frgrreg  30413  frgrregord013  30414  friendshipgt3  30417  isgrpo  30516  vciOLD  30580  vcex  30597  nmogtmnf  30789  siilem1  30870  siii  30872  ajmoi  30877  bcsiALT  31198  hhcms  31222  ocval  31299  hsupval  31353  omlsilem  31421  h1de2bi  31573  h1de2ctlem  31574  hosubeq0i  31845  adjmo  31851  nmopgtmnf  31887  nlfnval  31900  nmcopex  32048  nmcfnex  32072  riesz4i  32082  riesz1  32084  riesz2  32085  opsqrlem1  32159  superpos  32373  hatomistici  32381  chpssati  32382  mdsymlem3  32424  an42ds  32469  3o1cs  32480  3o2cs  32481  3o3cs  32482  iunrnmptss  32578  brabgaf  32620  f1mptrn  32645  ffsrn  32740  fpwrelmap  32744  xnn0gt0  32773  hashxpe  32811  elrgspnlem4  33249  prmidl2  33469  mxidlnzrb  33508  evl1deg2  33602  evl1deg3  33603  fedgmul  33682  ordtrest2NEWlem  33921  qqhval2  33983  esumfsup  34071  esumcvg  34087  cntnevol  34229  ddemeas  34237  dya2icoseg2  34280  dya2iocnei  34284  eulerpartlems  34362  eulerpartlemgvv  34378  eulerpart  34384  cndprobprob  34440  ballotlemsdom  34514  ballotth  34540  sgn3da  34544  bnj945  34787  bnj1379  34844  bnj1459  34857  bnj557  34915  bnj571  34920  bnj849  34939  bnj964  34957  bnj978  34963  bnj1018g  34977  bnj1018  34978  bnj1020  34979  bnj1033  34983  bnj1175  35018  bnj1398  35048  bnj1417  35055  bnj1523  35085  nummin  35105  cusgr3cyclex  35141  txpconn  35237  satfv1  35368  satffun  35414  msubco  35536  mclsax  35574  setinds  35779  dfon2lem7  35790  dfon2lem8  35791  pprodss4v  35885  fullfunfv  35948  altxpsspw  35978  funtransport  36032  fvtransport  36033  funray  36141  fvray  36142  funline  36143  fvline  36145  finminlem  36319  bisym1  36420  onsucconni  36438  onsucsuccmpi  36444  weiunse  36469  bj-currypara  36561  axc11n11r  36684  bj-equsal2  36826  bj-xpima1snALT  36958  bj-unexg  37039  bj-bm1.3ii  37065  bj-opelidb1ALT  37167  mptsnunlem  37339  iooelexlt  37363  relowlpssretop  37365  rdgeqoa  37371  difunieq  37375  nlpineqsn  37409  fvineqsneq  37413  wl-ax12v2cl  37507  wl-lem-nexmo  37568  matunitlindflem1  37623  ptrecube  37627  poimirlem26  37653  poimirlem30  37657  poimir  37660  ismblfin  37668  itg2addnclem  37678  dvasin  37711  sdclem2  37749  totbndbnd  37796  ismgmOLD  37857  exidresid  37886  isrngo  37904  rngoablo2  37916  rngoueqz  37947  isdivrngo  37957  isdrngo1  37963  isdrngo2  37965  ispridl2  38045  relcnveq3  38322  elrelscnveq3  38492  ax12eq  38942  ax12el  38943  lkr0f  39095  hl2at  39407  dalemswapyz  39658  pclfinclN  39952  osumcllem11N  39968  pexmidlem8N  39979  ltrnnid  40138  aks4d1p8  42088  redvmptabs  42390  sn-00id  42431  rictr  42530  eu6w  42686  mptfcl  42731  fphpd  42827  elmnc  43148  itgoval  43173  arearect  43227  reabsifpos  43647  clsk3nimkb  44053  grumnud  44305  nanorxor  44324  pm11.71  44416  iotavalsb  44452  sbiota1  44453  2uasbanh  44581  eel0TT  44724  eelT00  44725  eelTTT  44726  eelT11  44727  eelT12  44729  eelTT1  44730  eelT01  44731  eel0T1  44732  eelTT  44791  uunT1p1  44801  uun121  44803  uun121p1  44804  un2122  44810  uunTT1  44813  uunTT1p1  44814  uunTT1p2  44815  uunT11  44816  uunT11p1  44817  uunT11p2  44818  uunT12  44819  uunT12p1  44820  uunT12p2  44821  uunT12p3  44822  uunT12p4  44823  uunT12p5  44824  uun111  44825  3anidm12p2  44827  uun123  44828  3impdirp1  44836  undif3VD  44902  ax6e2ndeqVD  44929  2uasbanhVD  44931  ax6e2ndeqALT  44951  iunconnlem2  44955  sineq0ALT  44957  modelaxreplem1  44995  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem3  46018  stoweidlem17  46032  fourierdlem42  46164  fourierdlem48  46169  fourierdlem50  46171  fourierdlem51  46172  fourierdlem76  46197  fourierdlem83  46204  fourierdlem87  46208  hoidmvval0  46602  evenwodadd  46903  rexrsb  47112  2reu8i  47125  2reuimp  47127  afv0nbfvbi  47163  afvfv0bi  47164  afveu  47165  fnbrafvb  47166  afvres  47184  tz6.12-afv  47185  dmfcoafv  47187  afvco2  47188  aovprc  47200  aovrcl  47201  aovmpt4g  47213  afv2eu  47250  afv2res  47251  tz6.12-afv2  47252  tz6.12i-afv2  47255  afv2rnfveq  47274  fvmptrab  47304  fvmptrabdm  47305  fzopred  47334  2ffzoeq  47339  elsprel  47462  prproropf1o  47494  reupr  47509  lighneal  47598  odd2prm2  47705  even3prm2  47706  grictr  47892  grlimgrtrilem2  47962  usgrexmpl12ngric  47997  upgrwlkupwlk  48056  ovn0ssdmfun  48075  islinindfis  48366  rrx2linest  48663  line2ylem  48672  mofeu  48757  fucofvalne  49020  isthincd2  49086  setrec2fun  49211  elsetrecslem  49218  setrecsres  49221  secval  49266  cscval  49267  cotval  49268