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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylbb  123  sylbb2  138  3imtr4i  201  simplbiim  391  mpan10  478  an12s  571  an32s  574  an4s  596  sylnbi  689  dcim  853  notnotrdc  855  condcOLD  866  pm2.61ddc  873  pm5.18dc  895  pm2.25dc  905  pm2.85dc  917  pm5.12dc  922  pm5.14dc  923  pm5.55dc  925  peircedc  926  pm5.54dc  930  dcand  945  dcor  948  pm5.62dc  958  pm5.63dc  959  pm4.83dc  964  ifp2  993  ifpor  1000  1fpid3  1007  3simpb  1026  3simpc  1027  3imp  1224  3com12  1238  3com13  1239  syl3anb  1321  xoranor  1426  xorbin  1433  xordc1  1442  biassdc  1444  nfr  1571  nfand  1621  19.21t  1635  19.30dc  1680  exintrbi  1686  19.9t  1695  nfnt  1708  equveli  1812  exdistrfor  1853  sbcof2  1863  sbidm  1904  sbi1v  1946  sbalyz  2059  sbal1yz  2061  nfsb4t  2074  euex  2116  eumo0  2117  mor  2129  exmodc  2137  mo3h  2140  mopick  2165  moexexdc  2171  euexex  2172  2euex  2174  exists2  2184  eqcoms  2241  eleq2s  2333  nfcr  2384  necon3ai  2469  rexnalim  2539  dfrex2dc  2541  rexex  2596  rsp  2597  ralim  2609  rexim  2644  r19.32r  2697  r19.44av  2710  r19.45av  2711  gencl  2854  gencbvex  2869  gencbval  2871  vtoclgf  2881  vtoclg1f  2882  pm13.183  2964  elrabi  2979  eueq2dc  2999  eueq3dc  3000  mob2  3006  euxfr2dc  3011  reu3  3016  rmoim  3027  2rmorex  3032  sbcex  3060  sbcbi2  3102  ra5  3141  sseq1  3271  difdif  3354  dfss4st  3464  difindiss  3485  undif3ss  3492  dfrab3ss  3511  abvor0dc  3545  reldisj  3576  disjel  3579  inssdif0imOLD  3593  uneqdifeqim  3613  r19.2m  3614  r19.2mOLD  3615  r19.3rm  3616  r19.9rmv  3619  rexm  3627  ralm  3631  raaanlem  3632  ifnefalse  3651  ifnotdc  3679  ifandc  3681  ifmdc  3683  nelpri  3733  nelprd  3735  prprc1  3821  difprsn2  3855  diftpsn3  3856  snsssn  3886  preqr2  3894  preq12b  3895  opthpr  3897  prneimg  3899  oprcl  3928  pwprss  3931  intmin4  3998  uniintabim  4007  dfiin2g  4045  iinss2  4065  iundif2ss  4078  disjnim  4120  disjnims  4121  invdisj  4123  disjiun  4125  brne0  4181  brm  4182  trel  4238  trss  4240  ssex  4272  bnd2  4312  abssexg  4321  exmidexmid  4335  rext  4357  unipw  4359  euabex  4367  mss  4368  exss  4369  copsexg  4386  opelopabsb  4404  pwssunim  4431  epelg  4437  sowlin  4467  sotritric  4471  elsuci  4550  sucprc  4559  reusv3  4608  ordon  4635  onsucmin  4656  onsucelsucr  4657  unon  4660  onsucelsucexmid  4679  setind  4688  setind2  4689  sucprcreg  4698  en2lp  4703  eunex  4710  ordsoexmid  4711  ordpwsucss  4716  tfi  4731  peano1  4743  peano2  4744  find  4748  0nelelxp  4805  opelxp  4806  elvvuni  4841  optocl  4853  ralxpf  4928  rexxpf  4929  relop  4932  breldm  4987  reldmm  5002  dmxpm  5004  elreldm  5010  dmrnssfld  5047  dmcosseq  5056  resabs1  5094  resima2  5099  issref  5173  asymref  5176  xpidtr  5181  trin2  5182  poirr2  5183  xpmlem  5211  dmxpss  5221  xp11m  5229  cnveqb  5246  dfco2a  5291  cores2  5303  coi2  5307  relcnvtr  5310  relresfld  5320  relcnvexb  5330  cnviinm  5332  iotauni  5353  iota1  5355  iota4  5360  iotam  5372  dffun8  5408  fununfun  5427  funcnvsn  5429  imadif  5464  imainlem  5465  fcoi1  5575  fcoi2  5576  f0rn0  5590  f1ocnv  5655  f1ocnvb  5656  fun11iun  5663  ffoss  5675  f1o00  5679  fo00  5680  relelfvdm  5730  nfvres  5735  nfunsn  5736  ssimaex  5767  fvmptss2  5783  fvmptssdm  5793  unpreima  5836  respreima  5839  elrnrexdm  5850  elrnrexdmb  5851  rexrnmpt  5854  dffo4  5859  rnmptss  5872  funiun  5893  funopdmsn  5898  fvpr1  5922  fvpr2  5923  elunirn  5975  f1veqaeq  5978  isores1  6023  iotaexel  6046  riotauni  6048  riotacl2  6056  riota1  6061  riota1a  6062  snriota  6073  eusvobj2  6074  acexmidlema  6079  acexmidlemb  6080  acexmidlem2  6085  oprabid  6120  0neqopab  6136  brabvv  6137  1stval2  6393  2ndval2  6394  xp1st  6403  xp2nd  6404  unielxp  6412  releldm2  6423  cnvf1o  6465  fo2ndf  6467  poxp  6472  reldmtpos  6528  dftpos4  6538  tpostpos  6539  tpostpos2  6540  iunon  6559  smoel  6575  tfrlem4  6588  tfrlem7  6592  tfrlem8  6593  tfrlem9  6594  nnaord  6786  ecexr  6816  swoord1  6840  swoord2  6841  0er  6845  mapprc  6930  mapfoss  6951  fsetdmprc0  6954  mapsnconst  6981  ixpf  7007  mptelixpg  7021  idssen  7068  ener  7071  en0  7087  en1  7091  en1bg  7092  2dom  7098  modom  7113  enm  7123  xpsnen  7124  ssenen  7157  snnen2og  7165  php5dom  7169  phpm  7172  findcard  7197  findcard2  7198  findcard2s  7199  unfiexmid  7230  fiintim  7243  fidcenumlemim  7275  sbthlem1  7280  fiss  7317  djuexb  7391  djuss  7417  eldju2ndl  7419  eldju2ndr  7420  ctssdclemr  7459  exmidlpo  7490  finnum  7535  ficardon  7541  exmidfodomrlemim  7560  acnrcl  7564  3nsssucpw1  7602  indpi  7716  subhalfnqq  7788  archnqq  7791  enq0sym  7806  nqnq0pi  7812  nqnq0  7815  mulnnnq0  7824  prml  7851  prmu  7852  prssnql  7853  prssnqu  7854  prcdnql  7858  prcunqu  7859  prltlu  7861  prnmaxl  7862  prnminu  7863  prloc  7865  prdisj  7866  addcanprg  7990  recexprlemopl  7999  recexprlemopu  8001  cauappcvgprlemladdfu  8028  caucvgprlemladdfu  8051  recexgt0sr  8147  renfdisj  8392  axsuploc  8405  negf1o  8717  recexre  8915  apsqgt0  8938  apreim  8940  aprcl  8983  recexaplem2  8989  rerecclap  9069  nn0ge0  9600  elnnnn0b  9619  xnn0xr  9647  xnn0nemnf  9653  xnn0nnn0pnf  9655  znegcl  9687  zeo  9763  nn0ind  9772  nn0ind-raph  9775  uzn0  9955  eluzaddi  9966  eluzsubi  9967  uznn0sub  9971  uz3m2nn  9990  uznnssnn  9994  uz2m1nn  10022  uz2mulcl  10025  indstr2  10026  qmulz  10040  qre  10042  qnegcl  10053  qreccl  10059  rphalflt  10102  nn0ledivnn  10186  xrltnr  10199  nltpnft  10234  ngtmnft  10237  xrrebnd  10239  xnegcl  10252  xnegneg  10253  xltnegi  10255  xrpnfdc  10262  xrmnfdc  10263  xnegid  10279  xaddid1  10282  xnn0lenn0nn0  10285  xnn0xadd0  10287  xposdif  10302  elioore  10332  elfzuz2  10451  uzsubsubfz  10470  fzdisj  10475  fzmmmeqm  10482  elfz0ubfz0  10550  elfz0fzfz0  10551  fz0fzelfz0  10552  fz0fzdiffz0  10555  elfzmlbp  10557  difelfzle  10559  difelfznle  10560  nn0disj  10563  2ffzeq  10566  fzo1fzo0n0  10613  elfzo0z  10614  elfzo0le  10615  fzonmapblen  10617  fzofzim  10618  elfzodifsumelfzo  10637  elfzonlteqm1  10646  fzonn0p1p1  10649  elfzom1p1elfzo  10650  ssfzo12bi  10661  ubmelm1fzo  10662  fzind2  10676  subfzo0  10679  infssuzcldc  10686  rebtwn2z  10707  fldiv4p1lem1div2  10762  fldiv4lem1div2  10764  flqeqceilz  10777  zmodidfzoimp  10813  modfzo0difsn  10854  nnsinds  10904  nn0sinds  10905  expcl2lemap  11010  qexpclz  11019  zzlesq  11168  facp1  11191  facnn2  11195  faclbnd3  11204  bcn1  11219  hashfz0  11289  hashfibc  11306  hashf1lem2  11309  wrdf  11333  swrdswrdlem  11499  swrdswrd  11500  swrdccatin1  11520  pfxccatin12lem2a  11522  pfxccatin12lem1  11523  swrdccatin2  11524  pfxccatin12lem2  11526  pfxccatin12lem3  11527  pfxccatin12  11528  pfxccat3  11529  swrdccat  11530  swrdccat3blem  11534  cvg1nlemres  11774  rexanuz  11777  fclim  12086  climmo  12090  iser3shft  12138  fsumsplitsn  12203  fsum2dlemstep  12227  fisumcom2  12231  arisum  12291  arisum2  12292  prodmodc  12371  fprodfac  12408  fprod2dlemstep  12415  fprodcom2fi  12419  fprodsplitsn  12426  eftlub  12483  ef01bndlem  12549  sin01gt0  12555  cos01gt0  12556  sin02gt0  12557  dvdsdivcl  12643  addmodlteqALT  12652  odd2np1  12666  oddge22np1  12674  m1expe  12692  nn0enne  12695  nn0o1gt2  12698  nno  12699  ndvdsadd  12724  dfgcd2  12817  mulgcd  12819  algfx  12856  prmind2  12924  prm2orodd  12930  prmgt1  12937  oddprmgt2  12939  dfphi2  13028  nnnn0modprm0  13064  prm23lt5  13072  pythagtriplem2  13075  pcz  13141  dvdsprmpweqnn  13145  oddprmdvds  13163  prmunb  13171  4sqlem4  13201  4sqlem19  13218  ballotfilem2  13287  ballotfilem7  13338  evenennn  13343  fngzsum  13768  gzsumvalx  13769  dfgrp3me  13965  mulgnn0gzsum  13991  rngdi  14347  rngdir  14348  dvdsrcl2  14516  unitinvcl  14540  unitinvinv  14541  unitlinv  14543  unitrinv  14544  opprdrng  14730  rmodislmodlem  14797  rmodislmod  14798  zrhval  15062  psrbagf  15166  distop  15323  ntrss  15357  ssntr  15360  lmrcl  15430  txuni2  15494  txcn  15513  hmeocnvb  15556  xmetunirn  15596  blssioo  15791  divcnap  15803  cdivcncfap  15842  dedekindeulemlub  15858  dedekindicclemlub  15867  dvexp2  15950  elply2  15973  plyco  15997  pilem3  16022  sincosq1sgn  16065  sincosq2sgn  16066  sincosq3sgn  16067  sincosq4sgn  16068  sinq12gt0  16069  logfac  16138  birthdaylem1g  16237  fsumdvdsmul  16297  bpos1  16322  zabsle1  16335  lgsdir2lem4  16367  gausslemma2dlem0f  16390  gausslemma2dlem1a  16394  gausslemma2dlem2  16398  gausslemma2dlem3  16399  gausslemma2dlem4  16400  2lgslem1a1  16422  2lgslem3  16437  2lgsoddprmlem3  16447  2lgsoddprm  16449  2sqlem2  16451  2sqlem10  16461  vtxvalprc  16513  iedgvalprc  16514  upgrex  16561  umgredg  16603  ausgrusgrben  16626  usgruspgrben  16644  usgrislfuspgrdom  16648  uhgr2edg  16664  uspgredg2v  16679  griedg0ssusgr  16709  subusgr  16733  wlkv  16784  wlk1walkdom  16817  trlsv  16842  trlf1  16846  clwwlk1loop  16857  clwwlkext2edg  16880  umgr2cwwkdifex  16883  clwwlknonex2lem2  16896  clwwlknonex2e  16898  eupthv  16904  eupth2lem3lem4fi  16931  konigsberglem5  16950  bj-pm2.18st  16995  bj-dcstab  17001  decidi  17040  sumdc2  17044  bj-charfunbi  17054  bdel  17088  bdssex  17145  bj-indind  17175  findset  17188  wexmiddc  17259  wexmiddifxy  17263  idjudju  17264  nninfall  17270  trirec0  17312  neap0mkv  17338  alsex  17358  ralsex  17359