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  2382  equsex  2423  dfmoeu  2536  2mo  2649  axie2  2704  necon1bi  2961  necon1i  2966  r19.35  3096  spc2ed  3544  reu6  3673  rabssrabd  4024  uneqin  4230  difin0ss  4314  inelcm  4406  falseral0OLD  4456  raaan2  4463  difprsn1  4744  tppreqb  4749  n0snor2el  4777  unissint  4915  intminss  4917  dfiun2g  4973  iununi  5042  triin  5209  bm1.3iiOLD  5237  eusv2nf  5330  reusv3i  5339  axprglem  5371  axprg  5372  moabexOLD  5404  opelopabt  5478  eqrelrel  5744  opeliunxp2  5785  opelrn  5890  ssxpb  6130  xpima  6138  xpimasn  6141  dmsn0el  6167  relcnvtr  6224  relcoi2  6233  elsnxp  6247  reuop  6249  iotanul  6470  f1imadifssran  6576  dffv2  6927  fnfvrnss  7065  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  zfrep6OLD  7899  fo1stres  7959  fo2ndres  7960  bropopvvv  8031  bropfvvvv  8033  frxp  8067  poseq  8099  soseq  8100  opeliunxp2f  8151  mpoxopoveqd  8162  reldmtpos  8175  frrlem4  8230  tfrlem5  8310  tfrlem9  8315  tfr2  8328  rdgsuc  8354  oaordi  8472  oeordi  8514  omopthi  8588  on2recsov  8595  fvmptmap  8820  mptelixpg  8874  ener  8939  domtr  8945  unen  8983  undom  8994  dom0  9034  xpf1o  9068  mapen  9070  pssnn  9094  unfi  9096  ssfi  9098  ensymfib  9109  entrfil  9110  enfii  9111  domtrfil  9117  unxpdomlem3  9159  isinf  9166  frfi  9186  unblem1  9193  fofinf1o  9233  fsuppun  9291  elirrv  9503  inf3lem2  9539  inf3lem5  9542  cantnfp1lem1  9588  cantnfp1lem3  9590  tcmin  9649  setinds  9659  frr2  9673  r1ordg  9691  r1ord  9693  rankr1ai  9711  r1val3  9751  bndrank  9754  unbndrank  9755  rankr1b  9777  rankxplim3  9794  tcrank  9797  xpnum  9864  cardmin2  9912  infxpenlem  9924  fseqen  9938  dfac8clem  9943  alephsson  10011  alephfp  10019  dfac4  10033  kmlem6  10067  kmlem8  10069  kmlem9  10070  cflem  10156  infpssr  10219  fin1a2lem12  10322  axcc4  10350  axcc4dom  10352  ac6s2  10397  zornn0g  10416  cardidg  10459  unsnen  10464  pwcfsdom  10495  cfpwsdom  10496  gchpwdom  10582  r1tskina  10694  intgru  10726  indpi  10819  nqereu  10841  supsrlem  11023  letrii  11259  dfnn3  12160  zaddcl  12532  nn0ind  12588  fnn0ind  12592  ublbneg  12847  nn01to3  12855  infmrp1  13261  fz0  13456  fzo1fzo0n0  13632  elfzom1elp1fzo  13649  fzo0end  13675  elfznelfzo  13690  fzind2  13705  injresinjlem  13707  fleqceilz  13775  nnsinds  13912  nn0sinds  13913  faclbnd4lem1  14217  hashinf  14259  hasheqf1oi  14275  hashgt0elex  14325  hashgt23el  14348  hashfacen  14378  hash2prde  14394  hash2sspr  14413  fun2dmnop0  14428  iswrddm0  14462  swrdnnn0nd  14581  swrdnd0  14582  swrdlsw  14592  pfxn0  14611  pfxnd0  14613  swrdswrdlem  14628  pfxccatin12lem3  14656  pfxccat3  14658  pfxccat3a  14662  swrdccat3blem  14663  cshwsublen  14720  cshwidxmod  14727  repswcshw  14736  cshw1  14746  trclun  14938  dmtrclfv  14942  rediv  15055  imdiv  15062  fsump1i  15693  modfsummods  15717  bpolydiflem  15978  bpoly3  15982  bpoly4  15983  cos1bnd  16113  sinltx  16115  rpnnen2lem1  16140  rpnnen2lem2  16141  rpnnen2lem12  16151  odd2np1  16269  opoe  16291  omoe  16292  opeo  16293  omeo  16294  gcdcllem1  16427  gcdaddmlem  16452  dfgcd2  16474  algfx  16508  lcmledvds  16527  lcmfunsnlem  16569  lcmfun  16573  coprmprod  16589  coprmproddvdslem  16590  odzval  16720  odzdvds  16724  prmreclem5  16849  mul4sq  16883  prmgaplem5  16984  prmgaplem6  16985  imasaddfnlem  17450  mreexexlem4d  17571  joindmss  18301  meetdmss  18315  gictr  19209  cntzval  19254  symg2bas  19326  odfval  19465  efgsfo  19672  efgrelexlemb  19683  dprddomcld  19936  dprdsubg  19959  dprd2da  19977  lssacs  20920  cnfldinv  21359  pzriprnglem7  21444  ocvval  21624  selvval  22079  dmatmul  22440  mdetfval1  22533  mndifsplit  22579  fvmptnn04if  22792  toprntopon  22868  opnnei  23063  ordtbas2  23134  ordtrest2lem  23146  lmmo  23323  fincmp  23336  bwth  23353  txbas  23510  ptcnplem  23564  tx2ndc  23594  hmphtr  23726  fbun  23783  filconn  23826  ptcmplem5  23999  cnextcn  24010  utoptop  24177  ucncn  24227  metust  24501  cfilucfil  24502  elcncf1di  24840  xrhmeo  24891  phtpycc  24936  copco  24963  pcohtpylem  24964  pcopt  24967  pcopt2  24968  ncvsi  25096  ovolval  25418  iunmbl2  25502  itg2splitlem  25693  cpnfval  25877  plyval  26139  fta1  26256  aaliou2b  26289  tayl0  26309  ulmdvlem3  26351  radcnvlem2  26363  dvradcnv  26370  reeff1o  26397  sincosq1lem  26446  sincosq2sgn  26448  sincosq4sgn  26450  sinq12ge0  26457  logrncl  26516  eflog  26525  cxpge0  26632  logb1  26719  atanf  26830  atanbnd  26876  igamf  27001  igamcl  27002  lgsne0  27286  mul2sq  27370  2sqreultblem  27399  pntibnd  27544  ostth  27590  nobdaymin  27733  nocvxminlem  27734  cutlt  27912  norec2ov  27937  addsuniflem  27981  mulsuniflem  28129  oldfib  28357  zmulscld  28377  zseo  28402  z12addscl  28457  mpteleeOLD  28952  axlowdimlem9  29007  axlowdimlem12  29010  axcontlem2  29022  axcontlem12  29032  structgrssvtx  29081  structgrssiedg  29082  lpvtx  29125  nbuhgr  29400  nbumgr  29404  nbuhgr2vtx1edgblem  29408  nbgr0edglem  29413  nbgr1vtx  29415  uvtx01vtx  29454  prcliscplgr  29471  cusgrsizeinds  29510  sizusglecusglem2  29520  uhgrvd00  29592  fusgrregdegfi  29627  rusgr1vtxlem  29645  wlkeq  29691  wlk1walk  29696  uspgr2wlkeq  29703  wlklenvclwlk  29711  wlkreslem  29725  wlkdlem2  29739  wlkdlem4  29741  spthonepeq  29809  cyclnumvtx  29857  clwlkclwwlkflem  30063  clwlkclwwlkfolem  30066  clwlkclwwlkf  30067  clwwisshclwws  30074  clwwlkneq0  30088  3wlkdlem6  30224  eupth2eucrct  30276  eupth2lem1  30277  eupth2lem3lem7  30293  frgr3vlem1  30332  frgr3vlem2  30333  frgrncvvdeqlem8  30365  frgrncvvdeqlem9  30366  numclwwlk5  30447  frgrreg  30453  frgrregord013  30454  friendshipgt3  30457  isgrpo  30557  vciOLD  30621  vcex  30638  nmogtmnf  30830  siilem1  30911  siii  30913  ajmoi  30918  bcsiALT  31239  hhcms  31263  ocval  31340  hsupval  31394  omlsilem  31462  h1de2bi  31614  h1de2ctlem  31615  hosubeq0i  31886  adjmo  31892  nmopgtmnf  31928  nlfnval  31941  nmcopex  32089  nmcfnex  32113  riesz4i  32123  riesz1  32125  riesz2  32126  opsqrlem1  32200  superpos  32414  hatomistici  32422  chpssati  32423  mdsymlem3  32465  3o1cs  32519  3o2cs  32520  3o3cs  32521  iunrnmptss  32624  brabgaf  32668  f1mptrn  32697  ffsrn  32790  xnn0gt0  32832  hashxpe  32870  sgn3da  32898  elrgspnlem4  33311  prmidl2  33506  mxidlnzrb  33545  evl1deg2  33642  evl1deg3  33643  fedgmul  33781  cos9thpiminplylem2  33933  ordtrest2NEWlem  34072  qqhval2  34132  esumfsup  34220  esumcvg  34236  cntnevol  34378  ddemeas  34386  dya2icoseg2  34428  dya2iocnei  34432  eulerpartlems  34510  eulerpartlemgvv  34526  eulerpart  34532  cndprobprob  34588  ballotlemsdom  34662  ballotth  34688  bnj945  34922  bnj1379  34978  bnj1459  34991  bnj557  35049  bnj571  35054  bnj849  35073  bnj964  35091  bnj978  35097  bnj1018g  35111  bnj1018  35112  bnj1020  35113  bnj1033  35117  bnj1175  35152  bnj1398  35182  bnj1417  35189  bnj1523  35219  nummin  35242  r1omhf  35255  axprALT2  35259  fineqvnttrclselem1  35271  onvf1odlem4  35294  onvf1od  35295  cusgr3cyclex  35324  txpconn  35420  satfv1  35551  satffun  35597  msubco  35719  mclsax  35757  dfon2lem7  35975  dfon2lem8  35976  pprodss4v  36070  fullfunfv  36135  altxpsspw  36165  funtransport  36219  fvtransport  36220  funray  36328  fvray  36329  funline  36330  fvline  36332  finminlem  36506  bisym1  36607  onsucconni  36625  onsucsuccmpi  36631  weiunse  36656  bj-currypara  36822  bj-cbvaw  36933  axc11n11r  36978  bj-equsal2  37130  bj-xpima1snALT  37262  bj-unexg  37343  bj-bm1.3ii  37369  bj-axseprep  37379  bj-axreprepsep  37380  bj-opelidb1ALT  37478  mptsnunlem  37650  iooelexlt  37674  relowlpssretop  37676  rdgeqoa  37682  difunieq  37686  nlpineqsn  37720  fvineqsneq  37724  wl-ax12v2cl  37818  wl-lem-nexmo  37883  matunitlindflem1  37928  ptrecube  37932  poimirlem26  37958  poimirlem30  37962  poimir  37965  ismblfin  37973  itg2addnclem  37983  dvasin  38016  sdclem2  38054  totbndbnd  38101  ismgmOLD  38162  exidresid  38191  isrngo  38209  rngoablo2  38221  rngoueqz  38252  isdivrngo  38262  isdrngo1  38268  isdrngo2  38270  ispridl2  38350  relcnveq3  38639  elrelscnveq3  38939  disjimeceqim  39116  dmqsblocks  39279  ax12eq  39378  ax12el  39379  lkr0f  39531  hl2at  39842  dalemswapyz  40093  pclfinclN  40387  osumcllem11N  40403  pexmidlem8N  40414  ltrnnid  40573  aks4d1p8  42518  redvmptabs  42791  sn-00id  42832  rictr  42964  eu6w  43108  mptfcl  43151  fphpd  43247  elmnc  43567  itgoval  43592  arearect  43646  reabsifpos  44064  clsk3nimkb  44470  grumnud  44716  nanorxor  44735  pm11.71  44827  iotavalsb  44863  sbiota1  44864  2uasbanh  44991  eel0TT  45133  eelT00  45134  eelTTT  45135  eelT11  45136  eelT12  45138  eelTT1  45139  eelT01  45140  eel0T1  45141  eelTT  45200  uunT1p1  45210  uun121  45212  uun121p1  45213  un2122  45219  uunTT1  45222  uunTT1p1  45223  uunTT1p2  45224  uunT11  45225  uunT11p1  45226  uunT11p2  45227  uunT12  45228  uunT12p1  45229  uunT12p2  45230  uunT12p3  45231  uunT12p4  45232  uunT12p5  45233  uun111  45234  3anidm12p2  45236  uun123  45237  3impdirp1  45245  undif3VD  45311  ax6e2ndeqVD  45338  2uasbanhVD  45340  ax6e2ndeqALT  45360  iunconnlem2  45364  sineq0ALT  45366  modelaxreplem1  45408  permaxrep  45436  ioodvbdlimc1lem2  46364  ioodvbdlimc2lem  46366  stoweidlem3  46435  stoweidlem17  46449  fourierdlem42  46581  fourierdlem48  46586  fourierdlem50  46588  fourierdlem51  46589  fourierdlem76  46614  fourierdlem83  46621  fourierdlem87  46625  hoidmvval0  47019  evenwodadd  47319  rexrsb  47534  2reu8i  47547  2reuimp  47549  afv0nbfvbi  47585  afvfv0bi  47586  afveu  47587  fnbrafvb  47588  afvres  47606  tz6.12-afv  47607  dmfcoafv  47609  afvco2  47610  aovprc  47622  aovrcl  47623  aovmpt4g  47635  afv2eu  47672  afv2res  47673  tz6.12-afv2  47674  tz6.12i-afv2  47677  afv2rnfveq  47696  fvmptrab  47726  fvmptrabdm  47727  fzopred  47756  2ffzoeq  47761  elsprel  47909  prproropf1o  47941  reupr  47956  lighneal  48045  odd2prm2  48152  even3prm2  48153  grictr  48357  grlimgrtrilem2  48436  usgrexmpl12ngric  48472  gpgprismgr4cycllem8  48536  gpgprismgr4cycllem11  48539  pgnbgreunbgrlem2lem1  48548  upgrwlkupwlk  48574  ovn0ssdmfun  48593  islinindfis  48883  rrx2linest  49176  line2ylem  49185  mofeu  49281  homf0  49442  uobffth  49651  uobeqw  49652  initopropd  49676  termopropd  49677  zeroopropd  49678  fucofvalne  49758  isthincd2  49870  lanrcl  50054  ranrcl  50055  setrec2fun  50125  elsetrecslem  50132  setrecsres  50135  secval  50180  cscval  50181  cotval  50182