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  an42ds  1491  nanass  1511  19.38  1840  19.35  1878  19.8aw  2053  equsexv  2275  sbi2  2308  nfeqf2  2381  equsex  2422  dfmoeu  2535  2mo  2648  axie2  2703  necon1bi  2960  necon1i  2965  r19.35  3094  spc2ed  3555  reu6  3684  rabssrabd  4035  uneqin  4241  difin0ss  4325  inelcm  4417  falseral0OLD  4468  raaan2  4475  difprsn1  4756  tppreqb  4761  n0snor2el  4789  unissint  4927  intminss  4929  dfiun2g  4985  iununi  5054  triin  5221  bm1.3iiOLD  5247  eusv2nf  5340  reusv3i  5349  moabexOLD  5407  opelopabt  5480  eqrelrel  5746  opeliunxp2  5787  opelrn  5892  ssxpb  6132  xpima  6140  xpimasn  6143  dmsn0el  6169  relcnvtr  6226  relcoi2  6235  elsnxp  6249  reuop  6251  iotanul  6472  f1imadifssran  6578  dffv2  6929  fnfvrnss  7066  fressnfv  7105  fconst5  7152  f1mpt  7207  isocnv3  7278  f1owe  7299  ovprc  7396  fvmpopr2d  7520  onminesb  7738  onminsb  7739  onintrab  7741  onnminsb  7744  ordsuci  7753  onsucuni2  7776  tfindsg2  7804  zfrep6  7899  fo1stres  7959  fo2ndres  7960  bropopvvv  8032  bropfvvvv  8034  frxp  8068  poseq  8100  soseq  8101  opeliunxp2f  8152  mpoxopoveqd  8163  reldmtpos  8176  frrlem4  8231  tfrlem5  8311  tfrlem9  8316  tfr2  8329  rdgsuc  8355  oaordi  8473  oeordi  8515  omopthi  8589  on2recsov  8596  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  elirrv  9502  inf3lem2  9538  inf3lem5  9541  cantnfp1lem1  9587  cantnfp1lem3  9589  tcmin  9648  setinds  9658  frr2  9672  r1ordg  9690  r1ord  9692  rankr1ai  9710  r1val3  9750  bndrank  9753  unbndrank  9754  rankr1b  9776  rankxplim3  9793  tcrank  9796  xpnum  9863  cardmin2  9911  infxpenlem  9923  fseqen  9937  dfac8clem  9942  alephsson  10010  alephfp  10018  dfac4  10032  kmlem6  10066  kmlem8  10068  kmlem9  10069  cflem  10155  infpssr  10218  fin1a2lem12  10321  axcc4  10349  axcc4dom  10351  ac6s2  10396  zornn0g  10415  cardidg  10458  unsnen  10463  pwcfsdom  10494  cfpwsdom  10495  gchpwdom  10581  r1tskina  10693  intgru  10725  indpi  10818  nqereu  10840  supsrlem  11022  letrii  11258  dfnn3  12159  zaddcl  12531  nn0ind  12587  fnn0ind  12591  ublbneg  12846  nn01to3  12854  infmrp1  13260  fz0  13455  fzo1fzo0n0  13631  elfzom1elp1fzo  13648  fzo0end  13674  elfznelfzo  13689  fzind2  13704  injresinjlem  13706  fleqceilz  13774  nnsinds  13911  nn0sinds  13912  faclbnd4lem1  14216  hashinf  14258  hasheqf1oi  14274  hashgt0elex  14324  hashgt23el  14347  hashfacen  14377  hash2prde  14393  hash2sspr  14412  fun2dmnop0  14427  iswrddm0  14461  swrdnnn0nd  14580  swrdnd0  14581  swrdlsw  14591  pfxn0  14610  pfxnd0  14612  swrdswrdlem  14627  pfxccatin12lem3  14655  pfxccat3  14657  pfxccat3a  14661  swrdccat3blem  14662  cshwsublen  14719  cshwidxmod  14726  repswcshw  14735  cshw1  14745  trclun  14937  dmtrclfv  14941  rediv  15054  imdiv  15061  fsump1i  15692  modfsummods  15716  bpolydiflem  15977  bpoly3  15981  bpoly4  15982  cos1bnd  16112  sinltx  16114  rpnnen2lem1  16139  rpnnen2lem2  16140  rpnnen2lem12  16150  odd2np1  16268  opoe  16290  omoe  16291  opeo  16292  omeo  16293  gcdcllem1  16426  gcdaddmlem  16451  dfgcd2  16473  algfx  16507  lcmledvds  16526  lcmfunsnlem  16568  lcmfun  16572  coprmprod  16588  coprmproddvdslem  16589  odzval  16719  odzdvds  16723  prmreclem5  16848  mul4sq  16882  prmgaplem5  16983  prmgaplem6  16984  imasaddfnlem  17449  mreexexlem4d  17570  joindmss  18300  meetdmss  18314  gictr  19205  cntzval  19250  symg2bas  19322  odfval  19461  efgsfo  19668  efgrelexlemb  19679  dprddomcld  19932  dprdsubg  19955  dprd2da  19973  lssacs  20918  cnfldinv  21357  pzriprnglem7  21442  ocvval  21622  selvval  22078  dmatmul  22441  mdetfval1  22534  mndifsplit  22580  fvmptnn04if  22793  toprntopon  22869  opnnei  23064  ordtbas2  23135  ordtrest2lem  23147  lmmo  23324  fincmp  23337  bwth  23354  txbas  23511  ptcnplem  23565  tx2ndc  23595  hmphtr  23727  fbun  23784  filconn  23827  ptcmplem5  24000  cnextcn  24011  utoptop  24178  ucncn  24228  metust  24502  cfilucfil  24503  elcncf1di  24844  xrhmeo  24900  phtpycc  24946  copco  24974  pcohtpylem  24975  pcopt  24978  pcopt2  24979  ncvsi  25107  ovolval  25430  iunmbl2  25514  itg2splitlem  25705  cpnfval  25890  plyval  26154  fta1  26272  aaliou2b  26305  tayl0  26325  ulmdvlem3  26367  radcnvlem2  26379  dvradcnv  26386  reeff1o  26413  sincosq1lem  26462  sincosq2sgn  26464  sincosq4sgn  26466  sinq12ge0  26473  logrncl  26532  eflog  26541  cxpge0  26648  logb1  26735  atanf  26846  atanbnd  26892  igamf  27017  igamcl  27018  lgsne0  27302  mul2sq  27386  2sqreultblem  27415  pntibnd  27560  ostth  27606  nobdaymin  27749  nocvxminlem  27750  cutlt  27928  norec2ov  27953  addsuniflem  27997  mulsuniflem  28145  oldfib  28373  zmulscld  28393  zseo  28418  z12addscl  28473  mpteleeOLD  28968  axlowdimlem9  29023  axlowdimlem12  29026  axcontlem2  29038  axcontlem12  29048  structgrssvtx  29097  structgrssiedg  29098  lpvtx  29141  nbuhgr  29416  nbumgr  29420  nbuhgr2vtx1edgblem  29424  nbgr0edglem  29429  nbgr1vtx  29431  uvtx01vtx  29470  prcliscplgr  29487  cusgrsizeinds  29526  sizusglecusglem2  29536  uhgrvd00  29608  fusgrregdegfi  29643  rusgr1vtxlem  29661  wlkeq  29707  wlk1walk  29712  uspgr2wlkeq  29719  wlklenvclwlk  29727  wlkreslem  29741  wlkdlem2  29755  wlkdlem4  29757  spthonepeq  29825  cyclnumvtx  29873  clwlkclwwlkflem  30079  clwlkclwwlkfolem  30082  clwlkclwwlkf  30083  clwwisshclwws  30090  clwwlkneq0  30104  3wlkdlem6  30240  eupth2eucrct  30292  eupth2lem1  30293  eupth2lem3lem7  30309  frgr3vlem1  30348  frgr3vlem2  30349  frgrncvvdeqlem8  30381  frgrncvvdeqlem9  30382  numclwwlk5  30463  frgrreg  30469  frgrregord013  30470  friendshipgt3  30473  isgrpo  30572  vciOLD  30636  vcex  30653  nmogtmnf  30845  siilem1  30926  siii  30928  ajmoi  30933  bcsiALT  31254  hhcms  31278  ocval  31355  hsupval  31409  omlsilem  31477  h1de2bi  31629  h1de2ctlem  31630  hosubeq0i  31901  adjmo  31907  nmopgtmnf  31943  nlfnval  31956  nmcopex  32104  nmcfnex  32128  riesz4i  32138  riesz1  32140  riesz2  32141  opsqrlem1  32215  superpos  32429  hatomistici  32437  chpssati  32438  mdsymlem3  32480  3o1cs  32535  3o2cs  32536  3o3cs  32537  iunrnmptss  32640  brabgaf  32684  f1mptrn  32713  ffsrn  32807  xnn0gt0  32849  hashxpe  32887  sgn3da  32915  elrgspnlem4  33327  prmidl2  33522  mxidlnzrb  33561  evl1deg2  33658  evl1deg3  33659  fedgmul  33788  cos9thpiminplylem2  33940  ordtrest2NEWlem  34079  qqhval2  34139  esumfsup  34227  esumcvg  34243  cntnevol  34385  ddemeas  34393  dya2icoseg2  34435  dya2iocnei  34439  eulerpartlems  34517  eulerpartlemgvv  34533  eulerpart  34539  cndprobprob  34595  ballotlemsdom  34669  ballotth  34695  bnj945  34929  bnj1379  34986  bnj1459  34999  bnj557  35057  bnj571  35062  bnj849  35081  bnj964  35099  bnj978  35105  bnj1018g  35119  bnj1018  35120  bnj1020  35121  bnj1033  35125  bnj1175  35160  bnj1398  35190  bnj1417  35197  bnj1523  35227  nummin  35249  r1omhf  35262  fineqvnttrclselem1  35277  onvf1odlem4  35300  onvf1od  35301  cusgr3cyclex  35330  txpconn  35426  satfv1  35557  satffun  35603  msubco  35725  mclsax  35763  dfon2lem7  35981  dfon2lem8  35982  pprodss4v  36076  fullfunfv  36141  altxpsspw  36171  funtransport  36225  fvtransport  36226  funray  36334  fvray  36335  funline  36336  fvline  36338  finminlem  36512  bisym1  36613  onsucconni  36631  onsucsuccmpi  36637  weiunse  36662  bj-currypara  36760  axc11n11r  36884  bj-equsal2  37026  bj-xpima1snALT  37158  bj-unexg  37239  bj-bm1.3ii  37265  bj-opelidb1ALT  37371  mptsnunlem  37543  iooelexlt  37567  relowlpssretop  37569  rdgeqoa  37575  difunieq  37579  nlpineqsn  37613  fvineqsneq  37617  wl-ax12v2cl  37711  wl-lem-nexmo  37772  matunitlindflem1  37817  ptrecube  37821  poimirlem26  37847  poimirlem30  37851  poimir  37854  ismblfin  37862  itg2addnclem  37872  dvasin  37905  sdclem2  37943  totbndbnd  37990  ismgmOLD  38051  exidresid  38080  isrngo  38098  rngoablo2  38110  rngoueqz  38141  isdivrngo  38151  isdrngo1  38157  isdrngo2  38159  ispridl2  38239  relcnveq3  38522  elrelscnveq3  38810  dmqsblocks  39122  ax12eq  39211  ax12el  39212  lkr0f  39364  hl2at  39675  dalemswapyz  39926  pclfinclN  40220  osumcllem11N  40236  pexmidlem8N  40247  ltrnnid  40406  aks4d1p8  42351  redvmptabs  42625  sn-00id  42666  rictr  42785  eu6w  42929  mptfcl  42972  fphpd  43068  elmnc  43388  itgoval  43413  arearect  43467  reabsifpos  43885  clsk3nimkb  44291  grumnud  44537  nanorxor  44556  pm11.71  44648  iotavalsb  44684  sbiota1  44685  2uasbanh  44812  eel0TT  44954  eelT00  44955  eelTTT  44956  eelT11  44957  eelT12  44959  eelTT1  44960  eelT01  44961  eel0T1  44962  eelTT  45021  uunT1p1  45031  uun121  45033  uun121p1  45034  un2122  45040  uunTT1  45043  uunTT1p1  45044  uunTT1p2  45045  uunT11  45046  uunT11p1  45047  uunT11p2  45048  uunT12  45049  uunT12p1  45050  uunT12p2  45051  uunT12p3  45052  uunT12p4  45053  uunT12p5  45054  uun111  45055  3anidm12p2  45057  uun123  45058  3impdirp1  45066  undif3VD  45132  ax6e2ndeqVD  45159  2uasbanhVD  45161  ax6e2ndeqALT  45181  iunconnlem2  45185  sineq0ALT  45187  modelaxreplem1  45229  permaxrep  45257  ioodvbdlimc1lem2  46186  ioodvbdlimc2lem  46188  stoweidlem3  46257  stoweidlem17  46271  fourierdlem42  46403  fourierdlem48  46408  fourierdlem50  46410  fourierdlem51  46411  fourierdlem76  46436  fourierdlem83  46443  fourierdlem87  46447  hoidmvval0  46841  evenwodadd  47141  rexrsb  47356  2reu8i  47369  2reuimp  47371  afv0nbfvbi  47407  afvfv0bi  47408  afveu  47409  fnbrafvb  47410  afvres  47428  tz6.12-afv  47429  dmfcoafv  47431  afvco2  47432  aovprc  47444  aovrcl  47445  aovmpt4g  47457  afv2eu  47494  afv2res  47495  tz6.12-afv2  47496  tz6.12i-afv2  47499  afv2rnfveq  47518  fvmptrab  47548  fvmptrabdm  47549  fzopred  47578  2ffzoeq  47583  elsprel  47731  prproropf1o  47763  reupr  47778  lighneal  47867  odd2prm2  47974  even3prm2  47975  grictr  48179  grlimgrtrilem2  48258  usgrexmpl12ngric  48294  gpgprismgr4cycllem8  48358  gpgprismgr4cycllem11  48361  pgnbgreunbgrlem2lem1  48370  upgrwlkupwlk  48396  ovn0ssdmfun  48415  islinindfis  48705  rrx2linest  48998  line2ylem  49007  mofeu  49103  homf0  49264  uobffth  49473  uobeqw  49474  initopropd  49498  termopropd  49499  zeroopropd  49500  fucofvalne  49580  isthincd2  49692  lanrcl  49876  ranrcl  49877  setrec2fun  49947  elsetrecslem  49954  setrecsres  49957  secval  50002  cscval  50003  cotval  50004