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  2051  equsexv  2269  sbi2  2302  nfeqf2  2375  equsex  2416  dfmoeu  2529  2mo  2641  axie2  2696  necon1bi  2953  necon1i  2958  r19.35  3087  sbhypfOLD  3500  spc2ed  3556  reu6  3686  rabssrabd  4034  uneqin  4240  difin0ss  4324  inelcm  4416  rzal  4460  ralf0  4465  falseral0  4467  raaan2  4472  difprsn1  4751  tppreqb  4756  n0snor2el  4784  unissint  4922  intminss  4924  dfiun2g  4980  iununi  5048  triin  5215  bm1.3iiOLD  5241  eusv2nf  5334  reusv3i  5343  moabex  5402  opelopabt  5475  eqrelrel  5740  opeliunxp2  5781  opelrn  5885  ssxpb  6123  xpima  6131  xpimasn  6134  dmsn0el  6160  relcnvtr  6216  relcoi2  6225  elsnxp  6239  reuop  6241  iotanul  6462  f1imadifssran  6568  dffv2  6918  fnfvrnss  7055  fressnfv  7094  fconst5  7142  f1mpt  7198  isocnv3  7269  f1owe  7290  ovprc  7387  fvmpopr2d  7511  onminesb  7729  onminsb  7730  onintrab  7732  onnminsb  7735  ordsuci  7744  onsucuni2  7767  tfindsg2  7795  zfrep6  7890  fo1stres  7950  fo2ndres  7951  bropopvvv  8023  bropfvvvv  8025  frxp  8059  poseq  8091  soseq  8092  opeliunxp2f  8143  mpoxopoveqd  8154  reldmtpos  8167  frrlem4  8222  tfrlem5  8302  tfrlem9  8307  tfr2  8320  rdgsuc  8346  oaordi  8464  oeordi  8505  omopthi  8579  on2recsov  8586  fvmptmap  8808  mptelixpg  8862  ener  8926  domtr  8932  snfiOLD  8969  unen  8971  undom  8982  dom0  9022  xpf1o  9056  mapen  9058  pssnn  9082  unfi  9085  ssfi  9087  ensymfib  9098  entrfil  9099  enfii  9100  domtrfil  9106  unxpdomlem3  9147  isinf  9154  frfi  9174  unblem1  9181  fofinf1o  9222  fsuppun  9277  elirrv  9489  inf3lem2  9525  inf3lem5  9528  cantnfp1lem1  9574  cantnfp1lem3  9576  tcmin  9637  frr2  9656  r1ordg  9674  r1ord  9676  rankr1ai  9694  r1val3  9734  bndrank  9737  unbndrank  9738  rankr1b  9760  rankxplim3  9777  tcrank  9780  xpnum  9847  cardmin2  9895  infxpenlem  9907  fseqen  9921  dfac8clem  9926  alephsson  9994  alephfp  10002  dfac4  10016  kmlem6  10050  kmlem8  10052  kmlem9  10053  cflem  10139  infpssr  10202  fin1a2lem12  10305  axcc4  10333  axcc4dom  10335  ac6s2  10380  zornn0g  10399  cardidg  10442  unsnen  10447  pwcfsdom  10477  cfpwsdom  10478  gchpwdom  10564  r1tskina  10676  intgru  10708  indpi  10801  nqereu  10823  supsrlem  11005  letrii  11241  dfnn3  12142  zaddcl  12515  nn0ind  12571  fnn0ind  12575  ublbneg  12834  nn01to3  12842  infmrp1  13247  fz0  13442  fzo1fzo0n0  13618  elfzom1elp1fzo  13635  fzo0end  13661  elfznelfzo  13675  fzind2  13688  injresinjlem  13690  fleqceilz  13758  nnsinds  13895  nn0sinds  13896  faclbnd4lem1  14200  hashinf  14242  hasheqf1oi  14258  hashgt0elex  14308  hashgt23el  14331  hashfacen  14361  hash2prde  14377  hash2sspr  14396  fun2dmnop0  14411  iswrddm0  14445  swrdnnn0nd  14563  swrdnd0  14564  swrdlsw  14574  pfxn0  14593  pfxnd0  14595  swrdswrdlem  14610  pfxccatin12lem3  14638  pfxccat3  14640  pfxccat3a  14644  swrdccat3blem  14645  cshwsublen  14702  cshwidxmod  14709  repswcshw  14718  cshw1  14728  trclun  14921  dmtrclfv  14925  rediv  15038  imdiv  15045  fsump1i  15676  modfsummods  15700  bpolydiflem  15961  bpoly3  15965  bpoly4  15966  cos1bnd  16096  sinltx  16098  rpnnen2lem1  16123  rpnnen2lem2  16124  rpnnen2lem12  16134  odd2np1  16252  opoe  16274  omoe  16275  opeo  16276  omeo  16277  gcdcllem1  16410  gcdaddmlem  16435  dfgcd2  16457  algfx  16491  lcmledvds  16510  lcmfunsnlem  16552  lcmfun  16556  coprmprod  16572  coprmproddvdslem  16573  odzval  16703  odzdvds  16707  prmreclem5  16832  mul4sq  16866  prmgaplem5  16967  prmgaplem6  16968  imasaddfnlem  17432  mreexexlem4d  17553  joindmss  18283  meetdmss  18297  gictr  19155  cntzval  19200  symg2bas  19272  odfval  19411  efgsfo  19618  efgrelexlemb  19629  dprddomcld  19882  dprdsubg  19905  dprd2da  19923  lssacs  20870  cnfldinv  21309  pzriprnglem7  21394  ocvval  21574  selvval  22020  dmatmul  22382  mdetfval1  22475  mndifsplit  22521  fvmptnn04if  22734  toprntopon  22810  opnnei  23005  ordtbas2  23076  ordtrest2lem  23088  lmmo  23265  fincmp  23278  bwth  23295  txbas  23452  ptcnplem  23506  tx2ndc  23536  hmphtr  23668  fbun  23725  filconn  23768  ptcmplem5  23941  cnextcn  23952  utoptop  24120  ucncn  24170  metust  24444  cfilucfil  24445  elcncf1di  24786  xrhmeo  24842  phtpycc  24888  copco  24916  pcohtpylem  24917  pcopt  24920  pcopt2  24921  ncvsi  25049  ovolval  25372  iunmbl2  25456  itg2splitlem  25647  cpnfval  25832  plyval  26096  fta1  26214  aaliou2b  26247  tayl0  26267  ulmdvlem3  26309  radcnvlem2  26321  dvradcnv  26328  reeff1o  26355  sincosq1lem  26404  sincosq2sgn  26406  sincosq4sgn  26408  sinq12ge0  26415  logrncl  26474  eflog  26483  cxpge0  26590  logb1  26677  atanf  26788  atanbnd  26834  igamf  26959  igamcl  26960  lgsne0  27244  mul2sq  27328  2sqreultblem  27357  pntibnd  27502  ostth  27548  nobdaymin  27687  nocvxminlem  27688  cutlt  27845  norec2ov  27869  addsuniflem  27913  mulsuniflem  28057  zmulscld  28290  zseo  28314  zs12addscl  28354  mptelee  28840  axlowdimlem9  28895  axlowdimlem12  28898  axcontlem2  28910  axcontlem12  28920  structgrssvtx  28969  structgrssiedg  28970  lpvtx  29013  nbuhgr  29288  nbumgr  29292  nbuhgr2vtx1edgblem  29296  nbgr0edglem  29301  nbgr1vtx  29303  uvtx01vtx  29342  prcliscplgr  29359  cusgrsizeinds  29398  sizusglecusglem2  29408  uhgrvd00  29480  fusgrregdegfi  29515  rusgr1vtxlem  29533  wlkeq  29579  wlk1walk  29584  uspgr2wlkeq  29591  wlklenvclwlk  29599  wlkreslem  29613  wlkdlem2  29627  wlkdlem4  29629  spthonepeq  29697  cyclnumvtx  29745  clwlkclwwlkflem  29948  clwlkclwwlkfolem  29951  clwlkclwwlkf  29952  clwwisshclwws  29959  clwwlkneq0  29973  3wlkdlem6  30109  eupth2eucrct  30161  eupth2lem1  30162  eupth2lem3lem7  30178  frgr3vlem1  30217  frgr3vlem2  30218  frgrncvvdeqlem8  30250  frgrncvvdeqlem9  30251  numclwwlk5  30332  frgrreg  30338  frgrregord013  30339  friendshipgt3  30342  isgrpo  30441  vciOLD  30505  vcex  30522  nmogtmnf  30714  siilem1  30795  siii  30797  ajmoi  30802  bcsiALT  31123  hhcms  31147  ocval  31224  hsupval  31278  omlsilem  31346  h1de2bi  31498  h1de2ctlem  31499  hosubeq0i  31770  adjmo  31776  nmopgtmnf  31812  nlfnval  31825  nmcopex  31973  nmcfnex  31997  riesz4i  32007  riesz1  32009  riesz2  32010  opsqrlem1  32084  superpos  32298  hatomistici  32306  chpssati  32307  mdsymlem3  32349  an42ds  32394  3o1cs  32405  3o2cs  32406  3o3cs  32407  iunrnmptss  32509  brabgaf  32553  f1mptrn  32578  ffsrn  32672  fpwrelmap  32676  xnn0gt0  32712  hashxpe  32752  sgn3da  32779  elrgspnlem4  33185  prmidl2  33378  mxidlnzrb  33417  evl1deg2  33512  evl1deg3  33513  fedgmul  33598  cos9thpiminplylem2  33750  ordtrest2NEWlem  33889  qqhval2  33949  esumfsup  34037  esumcvg  34053  cntnevol  34195  ddemeas  34203  dya2icoseg2  34246  dya2iocnei  34250  eulerpartlems  34328  eulerpartlemgvv  34344  eulerpart  34350  cndprobprob  34406  ballotlemsdom  34480  ballotth  34506  bnj945  34740  bnj1379  34797  bnj1459  34810  bnj557  34868  bnj571  34873  bnj849  34892  bnj964  34910  bnj978  34916  bnj1018g  34930  bnj1018  34931  bnj1020  34932  bnj1033  34936  bnj1175  34971  bnj1398  35001  bnj1417  35008  bnj1523  35038  nummin  35058  fineqvnttrclselem1  35074  onvf1odlem4  35083  onvf1od  35084  cusgr3cyclex  35113  txpconn  35209  satfv1  35340  satffun  35386  msubco  35508  mclsax  35546  setinds  35756  dfon2lem7  35767  dfon2lem8  35768  pprodss4v  35862  fullfunfv  35925  altxpsspw  35955  funtransport  36009  fvtransport  36010  funray  36118  fvray  36119  funline  36120  fvline  36122  finminlem  36296  bisym1  36397  onsucconni  36415  onsucsuccmpi  36421  weiunse  36446  bj-currypara  36538  axc11n11r  36661  bj-equsal2  36803  bj-xpima1snALT  36935  bj-unexg  37016  bj-bm1.3ii  37042  bj-opelidb1ALT  37144  mptsnunlem  37316  iooelexlt  37340  relowlpssretop  37342  rdgeqoa  37348  difunieq  37352  nlpineqsn  37386  fvineqsneq  37390  wl-ax12v2cl  37484  wl-lem-nexmo  37545  matunitlindflem1  37600  ptrecube  37604  poimirlem26  37630  poimirlem30  37634  poimir  37637  ismblfin  37645  itg2addnclem  37655  dvasin  37688  sdclem2  37726  totbndbnd  37773  ismgmOLD  37834  exidresid  37863  isrngo  37881  rngoablo2  37893  rngoueqz  37924  isdivrngo  37934  isdrngo1  37940  isdrngo2  37942  ispridl2  38022  relcnveq3  38299  elrelscnveq3  38472  dmqsblocks  38835  ax12eq  38924  ax12el  38925  lkr0f  39077  hl2at  39388  dalemswapyz  39639  pclfinclN  39933  osumcllem11N  39949  pexmidlem8N  39960  ltrnnid  40119  aks4d1p8  42064  redvmptabs  42337  sn-00id  42378  rictr  42497  eu6w  42653  mptfcl  42697  fphpd  42793  elmnc  43113  itgoval  43138  arearect  43192  reabsifpos  43611  clsk3nimkb  44017  grumnud  44263  nanorxor  44282  pm11.71  44374  iotavalsb  44410  sbiota1  44411  2uasbanh  44539  eel0TT  44681  eelT00  44682  eelTTT  44683  eelT11  44684  eelT12  44686  eelTT1  44687  eelT01  44688  eel0T1  44689  eelTT  44748  uunT1p1  44758  uun121  44760  uun121p1  44761  un2122  44767  uunTT1  44770  uunTT1p1  44771  uunTT1p2  44772  uunT11  44773  uunT11p1  44774  uunT11p2  44775  uunT12  44776  uunT12p1  44777  uunT12p2  44778  uunT12p3  44779  uunT12p4  44780  uunT12p5  44781  uun111  44782  3anidm12p2  44784  uun123  44785  3impdirp1  44793  undif3VD  44859  ax6e2ndeqVD  44886  2uasbanhVD  44888  ax6e2ndeqALT  44908  iunconnlem2  44912  sineq0ALT  44914  modelaxreplem1  44956  permaxrep  44984  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  stoweidlem3  45988  stoweidlem17  46002  fourierdlem42  46134  fourierdlem48  46139  fourierdlem50  46141  fourierdlem51  46142  fourierdlem76  46167  fourierdlem83  46174  fourierdlem87  46178  hoidmvval0  46572  evenwodadd  46873  rexrsb  47088  2reu8i  47101  2reuimp  47103  afv0nbfvbi  47139  afvfv0bi  47140  afveu  47141  fnbrafvb  47142  afvres  47160  tz6.12-afv  47161  dmfcoafv  47163  afvco2  47164  aovprc  47176  aovrcl  47177  aovmpt4g  47189  afv2eu  47226  afv2res  47227  tz6.12-afv2  47228  tz6.12i-afv2  47231  afv2rnfveq  47250  fvmptrab  47280  fvmptrabdm  47281  fzopred  47310  2ffzoeq  47315  elsprel  47463  prproropf1o  47495  reupr  47510  lighneal  47599  odd2prm2  47706  even3prm2  47707  grictr  47911  grlimgrtrilem2  47990  usgrexmpl12ngric  48026  gpgprismgr4cycllem8  48090  gpgprismgr4cycllem11  48093  pgnbgreunbgrlem2lem1  48102  upgrwlkupwlk  48128  ovn0ssdmfun  48147  islinindfis  48438  rrx2linest  48731  line2ylem  48740  mofeu  48836  homf0  48998  uobffth  49207  uobeqw  49208  initopropd  49232  termopropd  49233  zeroopropd  49234  fucofvalne  49314  isthincd2  49426  lanrcl  49610  ranrcl  49611  setrec2fun  49681  elsetrecslem  49688  setrecsres  49691  secval  49736  cscval  49737  cotval  49738