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  678  dcim  841  notnotrdc  843  condcOLD  854  pm2.61ddc  861  pm5.18dc  883  pm2.25dc  893  pm2.85dc  905  pm5.12dc  910  pm5.14dc  911  pm5.55dc  913  peircedc  914  pm5.54dc  918  dcor  935  pm5.62dc  945  pm5.63dc  946  pm4.83dc  951  3simpb  995  3simpc  996  3imp  1193  3com12  1207  3com13  1208  syl3anb  1281  xoranor  1377  xorbin  1384  xordc1  1393  biassdc  1395  nfr  1516  nfand  1566  19.21t  1580  19.30dc  1625  exintrbi  1631  19.9t  1640  nfnt  1654  equveli  1757  exdistrfor  1798  sbcof2  1808  sbidm  1849  sbi1v  1889  sbalyz  1997  sbal1yz  1999  nfsb4t  2012  euex  2054  eumo0  2055  mor  2066  exmodc  2074  mo3h  2077  mopick  2102  moexexdc  2108  euexex  2109  2euex  2111  exists2  2121  eqcoms  2178  eleq2s  2270  nfcr  2309  necon3ai  2394  rexnalim  2464  dfrex2dc  2466  rexex  2521  rsp  2522  ralim  2534  rexim  2569  r19.32r  2621  r19.44av  2634  r19.45av  2635  gencl  2767  gencbvex  2781  gencbval  2783  vtoclgf  2793  vtoclg1f  2794  pm13.183  2873  elrabi  2888  eueq2dc  2908  eueq3dc  2909  mob2  2915  euxfr2dc  2920  reu3  2925  rmoim  2936  2rmorex  2941  sbcex  2969  sbcbi2  3011  ra5  3049  sseq1  3176  difdif  3258  dfss4st  3366  difindiss  3387  undif3ss  3394  dfrab3ss  3411  abvor0dc  3444  reldisj  3472  disjel  3475  inssdif0im  3488  uneqdifeqim  3506  r19.2m  3507  r19.2mOLD  3508  r19.3rm  3509  r19.9rmv  3512  rexm  3520  ralm  3525  raaanlem  3526  ifnefalse  3543  ifnotdc  3568  ifandc  3569  ifmdc  3571  nelpri  3613  nelprd  3615  prprc1  3697  difprsn2  3729  diftpsn3  3730  snsssn  3757  preqr2  3765  preq12b  3766  opthpr  3768  prneimg  3770  oprcl  3798  pwprss  3801  intmin4  3868  uniintabim  3877  dfiin2g  3915  iinss2  3934  iundif2ss  3947  disjnim  3989  disjnims  3990  invdisj  3992  disjiun  3993  brne0  4047  brm  4048  trel  4103  trss  4105  ssex  4135  bnd2  4168  abssexg  4177  exmidexmid  4191  rext  4209  unipw  4211  euabex  4219  mss  4220  exss  4221  copsexg  4238  opelopabsb  4254  pwssunim  4278  epelg  4284  sowlin  4314  sotritric  4318  elsuci  4397  sucprc  4406  reusv3  4454  ordon  4479  onsucmin  4500  onsucelsucr  4501  unon  4504  onsucelsucexmid  4523  setind  4532  setind2  4533  sucprcreg  4542  en2lp  4547  eunex  4554  ordsoexmid  4555  ordpwsucss  4560  tfi  4575  peano1  4587  peano2  4588  find  4592  0nelelxp  4649  opelxp  4650  elvvuni  4684  optocl  4696  ralxpf  4766  rexxpf  4767  relop  4770  breldm  4824  dmxpm  4840  elreldm  4846  dmrnssfld  4883  dmcosseq  4891  resabs1  4929  resima2  4934  issref  5003  asymref  5006  xpidtr  5011  trin2  5012  poirr2  5013  xpmlem  5041  dmxpss  5051  xp11m  5059  cnveqb  5076  dfco2a  5121  cores2  5133  coi2  5137  relcnvtr  5140  relresfld  5150  relcnvexb  5160  cnviinm  5162  iotauni  5182  iota1  5184  iota4  5188  iotam  5200  dffun8  5236  funcnvsn  5253  imadif  5288  imainlem  5289  fcoi1  5388  fcoi2  5389  f0rn0  5402  f1ocnv  5466  f1ocnvb  5467  fun11iun  5474  ffoss  5485  f1o00  5488  fo00  5489  relelfvdm  5539  nfvres  5540  nfunsn  5541  ssimaex  5569  fvmptss2  5583  fvmptssdm  5592  unpreima  5633  respreima  5636  elrnrexdm  5647  elrnrexdmb  5648  rexrnmpt  5651  dffo4  5656  rnmptss  5669  fvpr1  5712  fvpr2  5713  elunirn  5757  f1veqaeq  5760  isores1  5805  riotauni  5827  riotacl2  5834  riota1  5839  riota1a  5840  snriota  5850  eusvobj2  5851  acexmidlema  5856  acexmidlemb  5857  acexmidlem2  5862  oprabid  5897  0neqopab  5910  brabvv  5911  1stval2  6146  2ndval2  6147  xp1st  6156  xp2nd  6157  unielxp  6165  releldm2  6176  cnvf1o  6216  fo2ndf  6218  poxp  6223  reldmtpos  6244  dftpos4  6254  tpostpos  6255  tpostpos2  6256  iunon  6275  smoel  6291  tfrlem4  6304  tfrlem7  6308  tfrlem8  6309  tfrlem9  6310  nnaord  6500  ecexr  6530  swoord1  6554  swoord2  6555  0er  6559  mapprc  6642  mapsnconst  6684  ixpf  6710  mptelixpg  6724  idssen  6767  ener  6769  en0  6785  en1  6789  en1bg  6790  2dom  6795  enm  6810  xpsnen  6811  ssenen  6841  snnen2og  6849  php5dom  6853  phpm  6855  findcard  6878  findcard2  6879  findcard2s  6880  unfiexmid  6907  fiintim  6918  fidcenumlemim  6941  sbthlem1  6946  fiss  6966  djuexb  7033  djuss  7059  eldju2ndl  7061  eldju2ndr  7062  ctssdclemr  7101  exmidlpo  7131  finnum  7172  exmidfodomrlemim  7190  3nsssucpw1  7225  indpi  7316  subhalfnqq  7388  archnqq  7391  enq0sym  7406  nqnq0pi  7412  nqnq0  7415  mulnnnq0  7424  prml  7451  prmu  7452  prssnql  7453  prssnqu  7454  prcdnql  7458  prcunqu  7459  prltlu  7461  prnmaxl  7462  prnminu  7463  prloc  7465  prdisj  7466  addcanprg  7590  recexprlemopl  7599  recexprlemopu  7601  cauappcvgprlemladdfu  7628  caucvgprlemladdfu  7651  recexgt0sr  7747  renfdisj  7991  axsuploc  8004  negf1o  8313  recexre  8509  apsqgt0  8532  apreim  8534  aprcl  8577  recexaplem2  8582  rerecclap  8659  nn0ge0  9172  elnnnn0b  9191  xnn0xr  9215  xnn0nemnf  9221  xnn0nnn0pnf  9223  znegcl  9255  zeo  9329  nn0ind  9338  nn0ind-raph  9341  uzn0  9514  eluzaddi  9525  eluzsubi  9526  uznn0sub  9530  uz3m2nn  9544  uznnssnn  9548  uz2m1nn  9576  uz2mulcl  9579  indstr2  9580  qmulz  9594  qre  9596  qnegcl  9607  qreccl  9613  rphalflt  9652  nn0ledivnn  9736  xrltnr  9748  nltpnft  9783  ngtmnft  9786  xrrebnd  9788  xnegcl  9801  xnegneg  9802  xltnegi  9804  xrpnfdc  9811  xrmnfdc  9812  xnegid  9828  xaddid1  9831  xnn0lenn0nn0  9834  xnn0xadd0  9836  xposdif  9851  elioore  9881  elfzuz2  9997  uzsubsubfz  10015  fzdisj  10020  fzmmmeqm  10026  elfz0ubfz0  10093  elfz0fzfz0  10094  fz0fzelfz0  10095  fz0fzdiffz0  10098  elfzmlbp  10100  difelfzle  10102  difelfznle  10103  nn0disj  10106  2ffzeq  10109  fzo1fzo0n0  10151  elfzo0z  10152  elfzo0le  10153  fzonmapblen  10155  fzofzim  10156  elfzodifsumelfzo  10169  elfzonlteqm1  10178  fzonn0p1p1  10181  elfzom1p1elfzo  10182  ssfzo12bi  10193  ubmelm1fzo  10194  fzind2  10207  subfzo0  10210  rebtwn2z  10223  fldiv4p1lem1div2  10273  flqeqceilz  10286  zmodidfzoimp  10322  modfzo0difsn  10363  nnsinds  10411  nn0sinds  10412  expcl2lemap  10500  qexpclz  10509  facp1  10676  facnn2  10680  faclbnd3  10689  bcn1  10704  hashfz0  10771  cvg1nlemres  10960  rexanuz  10963  fclim  11268  climmo  11272  iser3shft  11320  fsumsplitsn  11384  fsum2dlemstep  11408  fisumcom2  11412  arisum  11472  arisum2  11473  prodmodc  11552  fprodfac  11589  fprod2dlemstep  11596  fprodcom2fi  11600  fprodsplitsn  11607  eftlub  11664  ef01bndlem  11730  sin01gt0  11735  cos01gt0  11736  sin02gt0  11737  dvdsdivcl  11821  addmodlteqALT  11830  odd2np1  11843  oddge22np1  11851  m1expe  11869  nn0enne  11872  nn0o1gt2  11875  nno  11876  ndvdsadd  11901  infssuzcldc  11917  dfgcd2  11980  mulgcd  11982  algfx  12017  prmind2  12085  prm2orodd  12091  prmgt1  12097  oddprmgt2  12099  dfphi2  12185  nnnn0modprm0  12220  prm23lt5  12228  pythagtriplem2  12231  pcz  12296  dvdsprmpweqnn  12300  oddprmdvds  12317  prmunb  12325  4sqlem4  12355  evenennn  12359  dfgrp3me  12829  distop  13136  ntrss  13170  ssntr  13173  lmrcl  13242  lmreltop  13244  txuni2  13307  txcn  13326  hmeocnvb  13369  xmetunirn  13409  blssioo  13596  divcnap  13606  cdivcncfap  13638  dedekindeulemlub  13649  dedekindicclemlub  13658  dvexp2  13727  pilem3  13755  sincosq1sgn  13798  sincosq2sgn  13799  sincosq3sgn  13800  sincosq4sgn  13801  sinq12gt0  13802  zabsle1  13951  lgsdir2lem4  13983  2sqlem2  14002  2sqlem10  14012  bj-pm2.18st  14042  bj-dcstab  14048  decidi  14087  sumdc2  14091  bj-charfunbi  14103  bdel  14137  bdssex  14194  bj-indind  14224  findset  14237  nninfall  14299  trirec0  14333