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  2957  elrabi  2972  eueq2dc  2992  eueq3dc  2993  mob2  2999  euxfr2dc  3004  reu3  3009  rmoim  3020  2rmorex  3025  sbcex  3053  sbcbi2  3095  ra5  3134  sseq1  3263  difdif  3346  dfss4st  3456  difindiss  3477  undif3ss  3484  dfrab3ss  3501  abvor0dc  3534  reldisj  3562  disjel  3565  inssdif0im  3578  uneqdifeqim  3597  r19.2m  3598  r19.2mOLD  3599  r19.3rm  3600  r19.9rmv  3603  rexm  3611  ralm  3615  raaanlem  3616  ifnefalse  3635  ifnotdc  3663  ifandc  3665  ifmdc  3667  nelpri  3715  nelprd  3717  prprc1  3802  difprsn2  3836  diftpsn3  3837  snsssn  3867  preqr2  3875  preq12b  3876  opthpr  3878  prneimg  3880  oprcl  3909  pwprss  3912  intmin4  3979  uniintabim  3988  dfiin2g  4026  iinss2  4046  iundif2ss  4059  disjnim  4101  disjnims  4102  invdisj  4104  disjiun  4106  brne0  4161  brm  4162  trel  4217  trss  4219  ssex  4249  bnd2  4288  abssexg  4297  exmidexmid  4311  rext  4333  unipw  4335  euabex  4343  mss  4344  exss  4345  copsexg  4362  opelopabsb  4380  pwssunim  4407  epelg  4413  sowlin  4443  sotritric  4447  elsuci  4526  sucprc  4535  reusv3  4583  ordon  4610  onsucmin  4631  onsucelsucr  4632  unon  4635  onsucelsucexmid  4654  setind  4663  setind2  4664  sucprcreg  4673  en2lp  4678  eunex  4685  ordsoexmid  4686  ordpwsucss  4691  tfi  4706  peano1  4718  peano2  4719  find  4723  0nelelxp  4780  opelxp  4781  elvvuni  4816  optocl  4828  ralxpf  4903  rexxpf  4904  relop  4907  breldm  4962  reldmm  4977  dmxpm  4979  elreldm  4985  dmrnssfld  5022  dmcosseq  5031  resabs1  5069  resima2  5074  issref  5147  asymref  5150  xpidtr  5155  trin2  5156  poirr2  5157  xpmlem  5185  dmxpss  5195  xp11m  5203  cnveqb  5220  dfco2a  5265  cores2  5277  coi2  5281  relcnvtr  5284  relresfld  5294  relcnvexb  5304  cnviinm  5306  iotauni  5327  iota1  5329  iota4  5334  iotam  5346  dffun8  5382  fununfun  5401  funcnvsn  5403  imadif  5438  imainlem  5439  fcoi1  5549  fcoi2  5550  f0rn0  5564  f1ocnv  5629  f1ocnvb  5630  fun11iun  5637  ffoss  5649  f1o00  5653  fo00  5654  relelfvdm  5704  nfvres  5708  nfunsn  5709  ssimaex  5740  fvmptss2  5754  fvmptssdm  5764  unpreima  5804  respreima  5807  elrnrexdm  5818  elrnrexdmb  5819  rexrnmpt  5822  dffo4  5827  rnmptss  5840  funiun  5861  funopdmsn  5866  fvpr1  5890  fvpr2  5891  elunirn  5941  f1veqaeq  5944  isores1  5989  iotaexel  6010  riotauni  6012  riotacl2  6020  riota1  6025  riota1a  6026  snriota  6037  eusvobj2  6038  acexmidlema  6043  acexmidlemb  6044  acexmidlem2  6049  oprabid  6084  0neqopab  6100  brabvv  6101  1stval2  6351  2ndval2  6352  xp1st  6361  xp2nd  6362  unielxp  6370  releldm2  6381  cnvf1o  6423  fo2ndf  6425  poxp  6430  reldmtpos  6486  dftpos4  6496  tpostpos  6497  tpostpos2  6498  iunon  6517  smoel  6533  tfrlem4  6546  tfrlem7  6550  tfrlem8  6551  tfrlem9  6552  nnaord  6744  ecexr  6774  swoord1  6798  swoord2  6799  0er  6803  mapprc  6888  mapsnconst  6931  ixpf  6957  mptelixpg  6971  idssen  7018  ener  7021  en0  7037  en1  7041  en1bg  7042  2dom  7048  modom  7063  enm  7073  xpsnen  7074  ssenen  7107  snnen2og  7115  php5dom  7119  phpm  7122  findcard  7147  findcard2  7148  findcard2s  7149  unfiexmid  7180  fiintim  7193  fidcenumlemim  7224  sbthlem1  7229  fiss  7266  djuexb  7337  djuss  7363  eldju2ndl  7365  eldju2ndr  7366  ctssdclemr  7405  exmidlpo  7436  finnum  7481  ficardon  7487  exmidfodomrlemim  7506  acnrcl  7510  3nsssucpw1  7548  indpi  7662  subhalfnqq  7734  archnqq  7737  enq0sym  7752  nqnq0pi  7758  nqnq0  7761  mulnnnq0  7770  prml  7797  prmu  7798  prssnql  7799  prssnqu  7800  prcdnql  7804  prcunqu  7805  prltlu  7807  prnmaxl  7808  prnminu  7809  prloc  7811  prdisj  7812  addcanprg  7936  recexprlemopl  7945  recexprlemopu  7947  cauappcvgprlemladdfu  7974  caucvgprlemladdfu  7997  recexgt0sr  8093  renfdisj  8338  axsuploc  8351  negf1o  8660  recexre  8857  apsqgt0  8880  apreim  8882  aprcl  8925  recexaplem2  8931  rerecclap  9009  nn0ge0  9526  elnnnn0b  9545  xnn0xr  9573  xnn0nemnf  9579  xnn0nnn0pnf  9581  znegcl  9613  zeo  9689  nn0ind  9698  nn0ind-raph  9701  uzn0  9876  eluzaddi  9887  eluzsubi  9888  uznn0sub  9892  uz3m2nn  9911  uznnssnn  9915  uz2m1nn  9943  uz2mulcl  9946  indstr2  9947  qmulz  9961  qre  9963  qnegcl  9974  qreccl  9980  rphalflt  10022  nn0ledivnn  10106  xrltnr  10118  nltpnft  10153  ngtmnft  10156  xrrebnd  10158  xnegcl  10171  xnegneg  10172  xltnegi  10174  xrpnfdc  10181  xrmnfdc  10182  xnegid  10198  xaddid1  10201  xnn0lenn0nn0  10204  xnn0xadd0  10206  xposdif  10221  elioore  10251  elfzuz2  10369  uzsubsubfz  10387  fzdisj  10392  fzmmmeqm  10398  elfz0ubfz0  10466  elfz0fzfz0  10467  fz0fzelfz0  10468  fz0fzdiffz0  10471  elfzmlbp  10473  difelfzle  10475  difelfznle  10476  nn0disj  10479  2ffzeq  10482  fzo1fzo0n0  10529  elfzo0z  10530  elfzo0le  10531  fzonmapblen  10533  fzofzim  10534  elfzodifsumelfzo  10553  elfzonlteqm1  10562  fzonn0p1p1  10565  elfzom1p1elfzo  10566  ssfzo12bi  10577  ubmelm1fzo  10578  fzind2  10592  subfzo0  10595  infssuzcldc  10602  rebtwn2z  10621  fldiv4p1lem1div2  10672  fldiv4lem1div2  10674  flqeqceilz  10687  zmodidfzoimp  10723  modfzo0difsn  10764  nnsinds  10814  nn0sinds  10815  expcl2lemap  10920  qexpclz  10929  zzlesq  11078  facp1  11100  facnn2  11104  faclbnd3  11113  bcn1  11128  hashfz0  11198  hashfibc  11215  wrdf  11238  swrdswrdlem  11404  swrdswrd  11405  swrdccatin1  11425  pfxccatin12lem2a  11427  pfxccatin12lem1  11428  swrdccatin2  11429  pfxccatin12lem2  11431  pfxccatin12lem3  11432  pfxccatin12  11433  pfxccat3  11434  swrdccat  11435  swrdccat3blem  11439  cvg1nlemres  11678  rexanuz  11681  fclim  11987  climmo  11991  iser3shft  12039  fsumsplitsn  12104  fsum2dlemstep  12128  fisumcom2  12132  arisum  12192  arisum2  12193  prodmodc  12272  fprodfac  12309  fprod2dlemstep  12316  fprodcom2fi  12320  fprodsplitsn  12327  eftlub  12384  ef01bndlem  12450  sin01gt0  12456  cos01gt0  12457  sin02gt0  12458  dvdsdivcl  12544  addmodlteqALT  12553  odd2np1  12567  oddge22np1  12575  m1expe  12593  nn0enne  12596  nn0o1gt2  12599  nno  12600  ndvdsadd  12625  dfgcd2  12718  mulgcd  12720  algfx  12757  prmind2  12825  prm2orodd  12831  prmgt1  12837  oddprmgt2  12839  dfphi2  12925  nnnn0modprm0  12961  prm23lt5  12969  pythagtriplem2  12972  pcz  13038  dvdsprmpweqnn  13042  oddprmdvds  13060  prmunb  13068  4sqlem4  13098  4sqlem19  13115  ballotfilem2  13153  evenennn  13165  fngsum  13622  igsumvalx  13623  dfgrp3me  13834  mulgnn0gsum  13866  rngdi  14105  rngdir  14106  dvdsrcl2  14266  unitinvcl  14290  unitinvinv  14291  unitlinv  14293  unitrinv  14294  opprdrng  14480  rmodislmodlem  14547  rmodislmod  14548  zrhval  14814  psrbagf  14867  distop  14999  ntrss  15033  ssntr  15036  lmrcl  15106  txuni2  15170  txcn  15189  hmeocnvb  15232  xmetunirn  15272  blssioo  15467  divcnap  15479  cdivcncfap  15518  dedekindeulemlub  15534  dedekindicclemlub  15543  dvexp2  15626  elply2  15649  plyco  15673  pilem3  15697  sincosq1sgn  15740  sincosq2sgn  15741  sincosq3sgn  15742  sincosq4sgn  15743  sinq12gt0  15744  fsumdvdsmul  15908  zabsle1  15921  lgsdir2lem4  15953  gausslemma2dlem0f  15976  gausslemma2dlem1a  15980  gausslemma2dlem2  15984  gausslemma2dlem3  15985  gausslemma2dlem4  15986  2lgslem1a1  16008  2lgslem3  16023  2lgsoddprmlem3  16033  2lgsoddprm  16035  2sqlem2  16037  2sqlem10  16047  vtxvalprc  16099  iedgvalprc  16100  upgrex  16147  umgredg  16189  ausgrusgrben  16212  usgruspgrben  16230  usgrislfuspgrdom  16234  uhgr2edg  16250  uspgredg2v  16265  griedg0ssusgr  16295  subusgr  16319  wlkv  16370  wlk1walkdom  16403  trlsv  16428  trlf1  16432  clwwlk1loop  16443  clwwlkext2edg  16466  umgr2cwwkdifex  16469  clwwlknonex2lem2  16482  clwwlknonex2e  16484  eupthv  16490  eupth2lem3lem4fi  16517  konigsberglem5  16536  bj-pm2.18st  16571  bj-dcstab  16577  decidi  16616  sumdc2  16620  bj-charfunbi  16630  bdel  16664  bdssex  16721  bj-indind  16751  findset  16764  nninfall  16836  trirec0  16877  neap0mkv  16904