Theorem sylbi 121

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
sylbi.1	⊢ (𝜑 ↔ 𝜓)
sylbi.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
sylbi	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 120	. 2 ⊢ (𝜑 → 𝜓)
3		sylbi.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbb  123  sylbb2  138  3imtr4i  201  simplbiim  387  mpan10  474  an12s  567  an32s  570  an4s  592  sylnbi  685  dcim  849  notnotrdc  851  condcOLD  862  pm2.61ddc  869  pm5.18dc  891  pm2.25dc  901  pm2.85dc  913  pm5.12dc  918  pm5.14dc  919  pm5.55dc  921  peircedc  922  pm5.54dc  926  dcand  941  dcor  944  pm5.62dc  954  pm5.63dc  955  pm4.83dc  960  ifp2  989  ifpor  996  1fpid3  1003  3simpb  1022  3simpc  1023  3imp  1220  3com12  1234  3com13  1235  syl3anb  1317  xoranor  1422  xorbin  1429  xordc1  1438  biassdc  1440  nfr  1567  nfand  1617  19.21t  1631  19.30dc  1676  exintrbi  1682  19.9t  1691  nfnt  1704  equveli  1808  exdistrfor  1849  sbcof2  1859  sbidm  1900  sbi1v  1942  sbalyz  2055  sbal1yz  2057  nfsb4t  2070  euex  2112  eumo0  2113  mor  2125  exmodc  2133  mo3h  2136  mopick  2161  moexexdc  2167  euexex  2168  2euex  2170  exists2  2180  eqcoms  2237  eleq2s  2329  nfcr  2378  necon3ai  2463  rexnalim  2533  dfrex2dc  2535  rexex  2590  rsp  2591  ralim  2603  rexim  2638  r19.32r  2691  r19.44av  2704  r19.45av  2705  gencl  2848  gencbvex  2863  gencbval  2865  vtoclgf  2875  vtoclg1f  2876  pm13.183  2958  elrabi  2973  eueq2dc  2993  eueq3dc  2994  mob2  3000  euxfr2dc  3005  reu3  3010  rmoim  3021  2rmorex  3026  sbcex  3054  sbcbi2  3096  ra5  3135  sseq1  3265  difdif  3348  dfss4st  3458  difindiss  3479  undif3ss  3486  dfrab3ss  3503  abvor0dc  3536  reldisj  3564  disjel  3567  inssdif0im  3580  uneqdifeqim  3599  r19.2m  3600  r19.2mOLD  3601  r19.3rm  3602  r19.9rmv  3605  rexm  3613  ralm  3617  raaanlem  3618  ifnefalse  3637  ifnotdc  3665  ifandc  3667  ifmdc  3669  nelpri  3718  nelprd  3720  prprc1  3805  difprsn2  3839  diftpsn3  3840  snsssn  3870  preqr2  3878  preq12b  3879  opthpr  3881  prneimg  3883  oprcl  3912  pwprss  3915  intmin4  3982  uniintabim  3991  dfiin2g  4029  iinss2  4049  iundif2ss  4062  disjnim  4104  disjnims  4105  invdisj  4107  disjiun  4109  brne0  4164  brm  4165  trel  4220  trss  4222  ssex  4252  bnd2  4291  abssexg  4300  exmidexmid  4314  rext  4336  unipw  4338  euabex  4346  mss  4347  exss  4348  copsexg  4365  opelopabsb  4383  pwssunim  4410  epelg  4416  sowlin  4446  sotritric  4450  elsuci  4529  sucprc  4538  reusv3  4586  ordon  4613  onsucmin  4634  onsucelsucr  4635  unon  4638  onsucelsucexmid  4657  setind  4666  setind2  4667  sucprcreg  4676  en2lp  4681  eunex  4688  ordsoexmid  4689  ordpwsucss  4694  tfi  4709  peano1  4721  peano2  4722  find  4726  0nelelxp  4783  opelxp  4784  elvvuni  4819  optocl  4831  ralxpf  4906  rexxpf  4907  relop  4910  breldm  4965  reldmm  4980  dmxpm  4982  elreldm  4988  dmrnssfld  5025  dmcosseq  5034  resabs1  5072  resima2  5077  issref  5150  asymref  5153  xpidtr  5158  trin2  5159  poirr2  5160  xpmlem  5188  dmxpss  5198  xp11m  5206  cnveqb  5223  dfco2a  5268  cores2  5280  coi2  5284  relcnvtr  5287  relresfld  5297  relcnvexb  5307  cnviinm  5309  iotauni  5330  iota1  5332  iota4  5337  iotam  5349  dffun8  5385  fununfun  5404  funcnvsn  5406  imadif  5441  imainlem  5442  fcoi1  5552  fcoi2  5553  f0rn0  5567  f1ocnv  5632  f1ocnvb  5633  fun11iun  5640  ffoss  5652  f1o00  5656  fo00  5657  relelfvdm  5707  nfvres  5711  nfunsn  5712  ssimaex  5743  fvmptss2  5757  fvmptssdm  5767  unpreima  5807  respreima  5810  elrnrexdm  5821  elrnrexdmb  5822  rexrnmpt  5825  dffo4  5830  rnmptss  5843  funiun  5864  funopdmsn  5869  fvpr1  5893  fvpr2  5894  elunirn  5945  f1veqaeq  5948  isores1  5993  iotaexel  6016  riotauni  6018  riotacl2  6026  riota1  6031  riota1a  6032  snriota  6043  eusvobj2  6044  acexmidlema  6049  acexmidlemb  6050  acexmidlem2  6055  oprabid  6090  0neqopab  6106  brabvv  6107  1stval2  6362  2ndval2  6363  xp1st  6372  xp2nd  6373  unielxp  6381  releldm2  6392  cnvf1o  6434  fo2ndf  6436  poxp  6441  reldmtpos  6497  dftpos4  6507  tpostpos  6508  tpostpos2  6509  iunon  6528  smoel  6544  tfrlem4  6557  tfrlem7  6561  tfrlem8  6562  tfrlem9  6563  nnaord  6755  ecexr  6785  swoord1  6809  swoord2  6810  0er  6814  mapprc  6899  mapsnconst  6942  ixpf  6968  mptelixpg  6982  idssen  7029  ener  7032  en0  7048  en1  7052  en1bg  7053  2dom  7059  modom  7074  enm  7084  xpsnen  7085  ssenen  7118  snnen2og  7126  php5dom  7130  phpm  7133  findcard  7158  findcard2  7159  findcard2s  7160  unfiexmid  7191  fiintim  7204  fidcenumlemim  7235  sbthlem1  7240  fiss  7277  djuexb  7348  djuss  7374  eldju2ndl  7376  eldju2ndr  7377  ctssdclemr  7416  exmidlpo  7447  finnum  7492  ficardon  7498  exmidfodomrlemim  7517  acnrcl  7521  3nsssucpw1  7559  indpi  7673  subhalfnqq  7745  archnqq  7748  enq0sym  7763  nqnq0pi  7769  nqnq0  7772  mulnnnq0  7781  prml  7808  prmu  7809  prssnql  7810  prssnqu  7811  prcdnql  7815  prcunqu  7816  prltlu  7818  prnmaxl  7819  prnminu  7820  prloc  7822  prdisj  7823  addcanprg  7947  recexprlemopl  7956  recexprlemopu  7958  cauappcvgprlemladdfu  7985  caucvgprlemladdfu  8008  recexgt0sr  8104  renfdisj  8349  axsuploc  8362  negf1o  8673  recexre  8870  apsqgt0  8893  apreim  8895  aprcl  8938  recexaplem2  8944  rerecclap  9024  nn0ge0  9541  elnnnn0b  9560  xnn0xr  9588  xnn0nemnf  9594  xnn0nnn0pnf  9596  znegcl  9628  zeo  9704  nn0ind  9713  nn0ind-raph  9716  uzn0  9891  eluzaddi  9902  eluzsubi  9903  uznn0sub  9907  uz3m2nn  9926  uznnssnn  9930  uz2m1nn  9958  uz2mulcl  9961  indstr2  9962  qmulz  9976  qre  9978  qnegcl  9989  qreccl  9995  rphalflt  10037  nn0ledivnn  10121  xrltnr  10134  nltpnft  10169  ngtmnft  10172  xrrebnd  10174  xnegcl  10187  xnegneg  10188  xltnegi  10190  xrpnfdc  10197  xrmnfdc  10198  xnegid  10214  xaddid1  10217  xnn0lenn0nn0  10220  xnn0xadd0  10222  xposdif  10237  elioore  10267  elfzuz2  10386  uzsubsubfz  10404  fzdisj  10409  fzmmmeqm  10416  elfz0ubfz0  10484  elfz0fzfz0  10485  fz0fzelfz0  10486  fz0fzdiffz0  10489  elfzmlbp  10491  difelfzle  10493  difelfznle  10494  nn0disj  10497  2ffzeq  10500  fzo1fzo0n0  10547  elfzo0z  10548  elfzo0le  10549  fzonmapblen  10551  fzofzim  10552  elfzodifsumelfzo  10571  elfzonlteqm1  10580  fzonn0p1p1  10583  elfzom1p1elfzo  10584  ssfzo12bi  10595  ubmelm1fzo  10596  fzind2  10610  subfzo0  10613  infssuzcldc  10620  rebtwn2z  10641  fldiv4p1lem1div2  10692  fldiv4lem1div2  10694  flqeqceilz  10707  zmodidfzoimp  10743  modfzo0difsn  10784  nnsinds  10834  nn0sinds  10835  expcl2lemap  10940  qexpclz  10949  zzlesq  11098  facp1  11120  facnn2  11124  faclbnd3  11133  bcn1  11148  hashfz0  11218  hashfibc  11235  wrdf  11258  swrdswrdlem  11424  swrdswrd  11425  swrdccatin1  11445  pfxccatin12lem2a  11447  pfxccatin12lem1  11448  swrdccatin2  11449  pfxccatin12lem2  11451  pfxccatin12lem3  11452  pfxccatin12  11453  pfxccat3  11454  swrdccat  11455  swrdccat3blem  11459  cvg1nlemres  11698  rexanuz  11701  fclim  12007  climmo  12011  iser3shft  12059  fsumsplitsn  12124  fsum2dlemstep  12148  fisumcom2  12152  arisum  12212  arisum2  12213  prodmodc  12292  fprodfac  12329  fprod2dlemstep  12336  fprodcom2fi  12340  fprodsplitsn  12347  eftlub  12404  ef01bndlem  12470  sin01gt0  12476  cos01gt0  12477  sin02gt0  12478  dvdsdivcl  12564  addmodlteqALT  12573  odd2np1  12587  oddge22np1  12595  m1expe  12613  nn0enne  12616  nn0o1gt2  12619  nno  12620  ndvdsadd  12645  dfgcd2  12738  mulgcd  12740  algfx  12777  prmind2  12845  prm2orodd  12851  prmgt1  12857  oddprmgt2  12859  dfphi2  12945  nnnn0modprm0  12981  prm23lt5  12989  pythagtriplem2  12992  pcz  13058  dvdsprmpweqnn  13062  oddprmdvds  13080  prmunb  13088  4sqlem4  13118  4sqlem19  13135  ballotfilem2  13175  ballotfilem7  13226  evenennn  13231  fngsum  13654  igsumvalx  13655  dfgrp3me  13858  mulgnn0gsum  13884  rngdi  14182  rngdir  14183  dvdsrcl2  14347  unitinvcl  14371  unitinvinv  14372  unitlinv  14374  unitrinv  14375  opprdrng  14561  rmodislmodlem  14627  rmodislmod  14628  zrhval  14894  psrbagf  14947  distop  15079  ntrss  15113  ssntr  15116  lmrcl  15186  txuni2  15250  txcn  15269  hmeocnvb  15312  xmetunirn  15352  blssioo  15547  divcnap  15559  cdivcncfap  15598  dedekindeulemlub  15614  dedekindicclemlub  15623  dvexp2  15706  elply2  15729  plyco  15753  pilem3  15777  sincosq1sgn  15820  sincosq2sgn  15821  sincosq3sgn  15822  sincosq4sgn  15823  sinq12gt0  15824  fsumdvdsmul  15988  zabsle1  16001  lgsdir2lem4  16033  gausslemma2dlem0f  16056  gausslemma2dlem1a  16060  gausslemma2dlem2  16064  gausslemma2dlem3  16065  gausslemma2dlem4  16066  2lgslem1a1  16088  2lgslem3  16103  2lgsoddprmlem3  16113  2lgsoddprm  16115  2sqlem2  16117  2sqlem10  16127  vtxvalprc  16179  iedgvalprc  16180  upgrex  16227  umgredg  16269  ausgrusgrben  16292  usgruspgrben  16310  usgrislfuspgrdom  16314  uhgr2edg  16330  uspgredg2v  16345  griedg0ssusgr  16375  subusgr  16399  wlkv  16450  wlk1walkdom  16483  trlsv  16508  trlf1  16512  clwwlk1loop  16523  clwwlkext2edg  16546  umgr2cwwkdifex  16549  clwwlknonex2lem2  16562  clwwlknonex2e  16564  eupthv  16570  eupth2lem3lem4fi  16597  konigsberglem5  16616  bj-pm2.18st  16661  bj-dcstab  16667  decidi  16706  sumdc2  16710  bj-charfunbi  16720  bdel  16754  bdssex  16811  bj-indind  16841  findset  16854  nninfall  16926  trirec0  16967  neap0mkv  16994