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  565  an32s  568  an4s  588  sylnbi  679  dcim  842  notnotrdc  844  condcOLD  855  pm2.61ddc  862  pm5.18dc  884  pm2.25dc  894  pm2.85dc  906  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  peircedc  915  pm5.54dc  919  dcand  934  dcor  937  pm5.62dc  947  pm5.63dc  948  pm4.83dc  953  3simpb  997  3simpc  998  3imp  1195  3com12  1209  3com13  1210  syl3anb  1292  xoranor  1388  xorbin  1395  xordc1  1404  biassdc  1406  nfr  1529  nfand  1579  19.21t  1593  19.30dc  1638  exintrbi  1644  19.9t  1653  nfnt  1667  equveli  1770  exdistrfor  1811  sbcof2  1821  sbidm  1862  sbi1v  1903  sbalyz  2011  sbal1yz  2013  nfsb4t  2026  euex  2068  eumo0  2069  mor  2080  exmodc  2088  mo3h  2091  mopick  2116  moexexdc  2122  euexex  2123  2euex  2125  exists2  2135  eqcoms  2192  eleq2s  2284  nfcr  2324  necon3ai  2409  rexnalim  2479  dfrex2dc  2481  rexex  2536  rsp  2537  ralim  2549  rexim  2584  r19.32r  2636  r19.44av  2649  r19.45av  2650  gencl  2784  gencbvex  2798  gencbval  2800  vtoclgf  2810  vtoclg1f  2811  pm13.183  2890  elrabi  2905  eueq2dc  2925  eueq3dc  2926  mob2  2932  euxfr2dc  2937  reu3  2942  rmoim  2953  2rmorex  2958  sbcex  2986  sbcbi2  3028  ra5  3066  sseq1  3193  difdif  3275  dfss4st  3383  difindiss  3404  undif3ss  3411  dfrab3ss  3428  abvor0dc  3461  reldisj  3489  disjel  3492  inssdif0im  3505  uneqdifeqim  3523  r19.2m  3524  r19.2mOLD  3525  r19.3rm  3526  r19.9rmv  3529  rexm  3537  ralm  3542  raaanlem  3543  ifnefalse  3560  ifnotdc  3586  ifandc  3587  ifmdc  3589  nelpri  3631  nelprd  3633  prprc1  3715  difprsn2  3747  diftpsn3  3748  snsssn  3776  preqr2  3784  preq12b  3785  opthpr  3787  prneimg  3789  oprcl  3817  pwprss  3820  intmin4  3887  uniintabim  3896  dfiin2g  3934  iinss2  3954  iundif2ss  3967  disjnim  4009  disjnims  4010  invdisj  4012  disjiun  4013  brne0  4067  brm  4068  trel  4123  trss  4125  ssex  4155  bnd2  4191  abssexg  4200  exmidexmid  4214  rext  4233  unipw  4235  euabex  4243  mss  4244  exss  4245  copsexg  4262  opelopabsb  4278  pwssunim  4302  epelg  4308  sowlin  4338  sotritric  4342  elsuci  4421  sucprc  4430  reusv3  4478  ordon  4503  onsucmin  4524  onsucelsucr  4525  unon  4528  onsucelsucexmid  4547  setind  4556  setind2  4557  sucprcreg  4566  en2lp  4571  eunex  4578  ordsoexmid  4579  ordpwsucss  4584  tfi  4599  peano1  4611  peano2  4612  find  4616  0nelelxp  4673  opelxp  4674  elvvuni  4708  optocl  4720  ralxpf  4791  rexxpf  4792  relop  4795  breldm  4849  dmxpm  4865  elreldm  4871  dmrnssfld  4908  dmcosseq  4916  resabs1  4954  resima2  4959  issref  5029  asymref  5032  xpidtr  5037  trin2  5038  poirr2  5039  xpmlem  5067  dmxpss  5077  xp11m  5085  cnveqb  5102  dfco2a  5147  cores2  5159  coi2  5163  relcnvtr  5166  relresfld  5176  relcnvexb  5186  cnviinm  5188  iotauni  5208  iota1  5210  iota4  5215  iotam  5227  dffun8  5263  funcnvsn  5280  imadif  5315  imainlem  5316  fcoi1  5415  fcoi2  5416  f0rn0  5429  f1ocnv  5493  f1ocnvb  5494  fun11iun  5501  ffoss  5512  f1o00  5515  fo00  5516  relelfvdm  5566  nfvres  5567  nfunsn  5568  ssimaex  5597  fvmptss2  5611  fvmptssdm  5620  unpreima  5661  respreima  5664  elrnrexdm  5675  elrnrexdmb  5676  rexrnmpt  5679  dffo4  5684  rnmptss  5697  fvpr1  5740  fvpr2  5741  elunirn  5787  f1veqaeq  5790  isores1  5835  riotauni  5857  riotacl2  5864  riota1  5869  riota1a  5870  snriota  5880  eusvobj2  5881  acexmidlema  5886  acexmidlemb  5887  acexmidlem2  5892  oprabid  5927  0neqopab  5940  brabvv  5941  1stval2  6179  2ndval2  6180  xp1st  6189  xp2nd  6190  unielxp  6198  releldm2  6209  cnvf1o  6249  fo2ndf  6251  poxp  6256  reldmtpos  6277  dftpos4  6287  tpostpos  6288  tpostpos2  6289  iunon  6308  smoel  6324  tfrlem4  6337  tfrlem7  6341  tfrlem8  6342  tfrlem9  6343  nnaord  6533  ecexr  6563  swoord1  6587  swoord2  6588  0er  6592  mapprc  6677  mapsnconst  6719  ixpf  6745  mptelixpg  6759  idssen  6802  ener  6804  en0  6820  en1  6824  en1bg  6825  2dom  6830  enm  6845  xpsnen  6846  ssenen  6878  snnen2og  6886  php5dom  6890  phpm  6892  findcard  6915  findcard2  6916  findcard2s  6917  unfiexmid  6945  fiintim  6956  fidcenumlemim  6980  sbthlem1  6985  fiss  7005  djuexb  7072  djuss  7098  eldju2ndl  7100  eldju2ndr  7101  ctssdclemr  7140  exmidlpo  7170  finnum  7211  exmidfodomrlemim  7229  3nsssucpw1  7264  indpi  7370  subhalfnqq  7442  archnqq  7445  enq0sym  7460  nqnq0pi  7466  nqnq0  7469  mulnnnq0  7478  prml  7505  prmu  7506  prssnql  7507  prssnqu  7508  prcdnql  7512  prcunqu  7513  prltlu  7515  prnmaxl  7516  prnminu  7517  prloc  7519  prdisj  7520  addcanprg  7644  recexprlemopl  7653  recexprlemopu  7655  cauappcvgprlemladdfu  7682  caucvgprlemladdfu  7705  recexgt0sr  7801  renfdisj  8046  axsuploc  8059  negf1o  8368  recexre  8564  apsqgt0  8587  apreim  8589  aprcl  8632  recexaplem2  8638  rerecclap  8716  nn0ge0  9230  elnnnn0b  9249  xnn0xr  9273  xnn0nemnf  9279  xnn0nnn0pnf  9281  znegcl  9313  zeo  9387  nn0ind  9396  nn0ind-raph  9399  uzn0  9572  eluzaddi  9583  eluzsubi  9584  uznn0sub  9588  uz3m2nn  9602  uznnssnn  9606  uz2m1nn  9634  uz2mulcl  9637  indstr2  9638  qmulz  9652  qre  9654  qnegcl  9665  qreccl  9671  rphalflt  9712  nn0ledivnn  9796  xrltnr  9808  nltpnft  9843  ngtmnft  9846  xrrebnd  9848  xnegcl  9861  xnegneg  9862  xltnegi  9864  xrpnfdc  9871  xrmnfdc  9872  xnegid  9888  xaddid1  9891  xnn0lenn0nn0  9894  xnn0xadd0  9896  xposdif  9911  elioore  9941  elfzuz2  10058  uzsubsubfz  10076  fzdisj  10081  fzmmmeqm  10087  elfz0ubfz0  10154  elfz0fzfz0  10155  fz0fzelfz0  10156  fz0fzdiffz0  10159  elfzmlbp  10161  difelfzle  10163  difelfznle  10164  nn0disj  10167  2ffzeq  10170  fzo1fzo0n0  10212  elfzo0z  10213  elfzo0le  10214  fzonmapblen  10216  fzofzim  10217  elfzodifsumelfzo  10230  elfzonlteqm1  10239  fzonn0p1p1  10242  elfzom1p1elfzo  10243  ssfzo12bi  10254  ubmelm1fzo  10255  fzind2  10268  subfzo0  10271  rebtwn2z  10284  fldiv4p1lem1div2  10335  flqeqceilz  10348  zmodidfzoimp  10384  modfzo0difsn  10425  nnsinds  10473  nn0sinds  10474  expcl2lemap  10562  qexpclz  10571  zzlesq  10719  facp1  10741  facnn2  10745  faclbnd3  10754  bcn1  10769  hashfz0  10836  cvg1nlemres  11025  rexanuz  11028  fclim  11333  climmo  11337  iser3shft  11385  fsumsplitsn  11449  fsum2dlemstep  11473  fisumcom2  11477  arisum  11537  arisum2  11538  prodmodc  11617  fprodfac  11654  fprod2dlemstep  11661  fprodcom2fi  11665  fprodsplitsn  11672  eftlub  11729  ef01bndlem  11795  sin01gt0  11800  cos01gt0  11801  sin02gt0  11802  dvdsdivcl  11887  addmodlteqALT  11896  odd2np1  11909  oddge22np1  11917  m1expe  11935  nn0enne  11938  nn0o1gt2  11941  nno  11942  ndvdsadd  11967  infssuzcldc  11983  dfgcd2  12046  mulgcd  12048  algfx  12083  prmind2  12151  prm2orodd  12157  prmgt1  12163  oddprmgt2  12165  dfphi2  12251  nnnn0modprm0  12286  prm23lt5  12294  pythagtriplem2  12297  pcz  12363  dvdsprmpweqnn  12367  oddprmdvds  12385  prmunb  12393  4sqlem4  12423  4sqlem19  12440  evenennn  12443  dfgrp3me  13041  rngdi  13291  rngdir  13292  dvdsrcl2  13446  unitinvcl  13470  unitinvinv  13471  unitlinv  13473  unitrinv  13474  rmodislmodlem  13663  rmodislmod  13664  psrbagf  13945  distop  14037  ntrss  14071  ssntr  14074  lmrcl  14143  lmreltop  14145  txuni2  14208  txcn  14227  hmeocnvb  14270  xmetunirn  14310  blssioo  14497  divcnap  14507  cdivcncfap  14539  dedekindeulemlub  14550  dedekindicclemlub  14559  dvexp2  14628  pilem3  14656  sincosq1sgn  14699  sincosq2sgn  14700  sincosq3sgn  14701  sincosq4sgn  14702  sinq12gt0  14703  zabsle1  14853  lgsdir2lem4  14885  2lgsoddprmlem3  14912  2sqlem2  14915  2sqlem10  14925  bj-pm2.18st  14955  bj-dcstab  14961  decidi  15000  sumdc2  15004  bj-charfunbi  15016  bdel  15050  bdssex  15107  bj-indind  15137  findset  15150  nninfall  15212  trirec0  15246  neap0mkv  15271