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	|- ( ph <-> ps )
sylbi.2	|- ( ps -> ch )

Assertion

Ref	Expression
sylbi	|- ( ph -> ch )

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 |- ( ph <-> ps )
2	1	biimpi 120	. 2 |- ( ph -> ps )
3		sylbi.2	. 2 |- ( ps -> ch )
4	2, 3	syl 14	1 |- ( ph -> ch )

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  1518  nfand  1568  19.21t  1582  19.30dc  1627  exintrbi  1633  19.9t  1642  nfnt  1656  equveli  1759  exdistrfor  1800  sbcof2  1810  sbidm  1851  sbi1v  1891  sbalyz  1999  sbal1yz  2001  nfsb4t  2014  euex  2056  eumo0  2057  mor  2068  exmodc  2076  mo3h  2079  mopick  2104  moexexdc  2110  euexex  2111  2euex  2113  exists2  2123  eqcoms  2180  eleq2s  2272  nfcr  2311  necon3ai  2396  rexnalim  2466  dfrex2dc  2468  rexex  2523  rsp  2524  ralim  2536  rexim  2571  r19.32r  2623  r19.44av  2636  r19.45av  2637  gencl  2769  gencbvex  2783  gencbval  2785  vtoclgf  2795  vtoclg1f  2796  pm13.183  2875  elrabi  2890  eueq2dc  2910  eueq3dc  2911  mob2  2917  euxfr2dc  2922  reu3  2927  rmoim  2938  2rmorex  2943  sbcex  2971  sbcbi2  3013  ra5  3051  sseq1  3178  difdif  3260  dfss4st  3368  difindiss  3389  undif3ss  3396  dfrab3ss  3413  abvor0dc  3446  reldisj  3474  disjel  3477  inssdif0im  3490  uneqdifeqim  3508  r19.2m  3509  r19.2mOLD  3510  r19.3rm  3511  r19.9rmv  3514  rexm  3522  ralm  3527  raaanlem  3528  ifnefalse  3545  ifnotdc  3571  ifandc  3572  ifmdc  3574  nelpri  3616  nelprd  3618  prprc1  3700  difprsn2  3732  diftpsn3  3733  snsssn  3761  preqr2  3769  preq12b  3770  opthpr  3772  prneimg  3774  oprcl  3802  pwprss  3805  intmin4  3872  uniintabim  3881  dfiin2g  3919  iinss2  3939  iundif2ss  3952  disjnim  3994  disjnims  3995  invdisj  3997  disjiun  3998  brne0  4052  brm  4053  trel  4108  trss  4110  ssex  4140  bnd2  4173  abssexg  4182  exmidexmid  4196  rext  4215  unipw  4217  euabex  4225  mss  4226  exss  4227  copsexg  4244  opelopabsb  4260  pwssunim  4284  epelg  4290  sowlin  4320  sotritric  4324  elsuci  4403  sucprc  4412  reusv3  4460  ordon  4485  onsucmin  4506  onsucelsucr  4507  unon  4510  onsucelsucexmid  4529  setind  4538  setind2  4539  sucprcreg  4548  en2lp  4553  eunex  4560  ordsoexmid  4561  ordpwsucss  4566  tfi  4581  peano1  4593  peano2  4594  find  4598  0nelelxp  4655  opelxp  4656  elvvuni  4690  optocl  4702  ralxpf  4773  rexxpf  4774  relop  4777  breldm  4831  dmxpm  4847  elreldm  4853  dmrnssfld  4890  dmcosseq  4898  resabs1  4936  resima2  4941  issref  5011  asymref  5014  xpidtr  5019  trin2  5020  poirr2  5021  xpmlem  5049  dmxpss  5059  xp11m  5067  cnveqb  5084  dfco2a  5129  cores2  5141  coi2  5145  relcnvtr  5148  relresfld  5158  relcnvexb  5168  cnviinm  5170  iotauni  5190  iota1  5192  iota4  5196  iotam  5208  dffun8  5244  funcnvsn  5261  imadif  5296  imainlem  5297  fcoi1  5396  fcoi2  5397  f0rn0  5410  f1ocnv  5474  f1ocnvb  5475  fun11iun  5482  ffoss  5493  f1o00  5496  fo00  5497  relelfvdm  5547  nfvres  5548  nfunsn  5549  ssimaex  5577  fvmptss2  5591  fvmptssdm  5600  unpreima  5641  respreima  5644  elrnrexdm  5655  elrnrexdmb  5656  rexrnmpt  5659  dffo4  5664  rnmptss  5677  fvpr1  5720  fvpr2  5721  elunirn  5766  f1veqaeq  5769  isores1  5814  riotauni  5836  riotacl2  5843  riota1  5848  riota1a  5849  snriota  5859  eusvobj2  5860  acexmidlema  5865  acexmidlemb  5866  acexmidlem2  5871  oprabid  5906  0neqopab  5919  brabvv  5920  1stval2  6155  2ndval2  6156  xp1st  6165  xp2nd  6166  unielxp  6174  releldm2  6185  cnvf1o  6225  fo2ndf  6227  poxp  6232  reldmtpos  6253  dftpos4  6263  tpostpos  6264  tpostpos2  6265  iunon  6284  smoel  6300  tfrlem4  6313  tfrlem7  6317  tfrlem8  6318  tfrlem9  6319  nnaord  6509  ecexr  6539  swoord1  6563  swoord2  6564  0er  6568  mapprc  6651  mapsnconst  6693  ixpf  6719  mptelixpg  6733  idssen  6776  ener  6778  en0  6794  en1  6798  en1bg  6799  2dom  6804  enm  6819  xpsnen  6820  ssenen  6850  snnen2og  6858  php5dom  6862  phpm  6864  findcard  6887  findcard2  6888  findcard2s  6889  unfiexmid  6916  fiintim  6927  fidcenumlemim  6950  sbthlem1  6955  fiss  6975  djuexb  7042  djuss  7068  eldju2ndl  7070  eldju2ndr  7071  ctssdclemr  7110  exmidlpo  7140  finnum  7181  exmidfodomrlemim  7199  3nsssucpw1  7234  indpi  7340  subhalfnqq  7412  archnqq  7415  enq0sym  7430  nqnq0pi  7436  nqnq0  7439  mulnnnq0  7448  prml  7475  prmu  7476  prssnql  7477  prssnqu  7478  prcdnql  7482  prcunqu  7483  prltlu  7485  prnmaxl  7486  prnminu  7487  prloc  7489  prdisj  7490  addcanprg  7614  recexprlemopl  7623  recexprlemopu  7625  cauappcvgprlemladdfu  7652  caucvgprlemladdfu  7675  recexgt0sr  7771  renfdisj  8016  axsuploc  8029  negf1o  8338  recexre  8534  apsqgt0  8557  apreim  8559  aprcl  8602  recexaplem2  8608  rerecclap  8686  nn0ge0  9200  elnnnn0b  9219  xnn0xr  9243  xnn0nemnf  9249  xnn0nnn0pnf  9251  znegcl  9283  zeo  9357  nn0ind  9366  nn0ind-raph  9369  uzn0  9542  eluzaddi  9553  eluzsubi  9554  uznn0sub  9558  uz3m2nn  9572  uznnssnn  9576  uz2m1nn  9604  uz2mulcl  9607  indstr2  9608  qmulz  9622  qre  9624  qnegcl  9635  qreccl  9641  rphalflt  9682  nn0ledivnn  9766  xrltnr  9778  nltpnft  9813  ngtmnft  9816  xrrebnd  9818  xnegcl  9831  xnegneg  9832  xltnegi  9834  xrpnfdc  9841  xrmnfdc  9842  xnegid  9858  xaddid1  9861  xnn0lenn0nn0  9864  xnn0xadd0  9866  xposdif  9881  elioore  9911  elfzuz2  10028  uzsubsubfz  10046  fzdisj  10051  fzmmmeqm  10057  elfz0ubfz0  10124  elfz0fzfz0  10125  fz0fzelfz0  10126  fz0fzdiffz0  10129  elfzmlbp  10131  difelfzle  10133  difelfznle  10134  nn0disj  10137  2ffzeq  10140  fzo1fzo0n0  10182  elfzo0z  10183  elfzo0le  10184  fzonmapblen  10186  fzofzim  10187  elfzodifsumelfzo  10200  elfzonlteqm1  10209  fzonn0p1p1  10212  elfzom1p1elfzo  10213  ssfzo12bi  10224  ubmelm1fzo  10225  fzind2  10238  subfzo0  10241  rebtwn2z  10254  fldiv4p1lem1div2  10304  flqeqceilz  10317  zmodidfzoimp  10353  modfzo0difsn  10394  nnsinds  10442  nn0sinds  10443  expcl2lemap  10531  qexpclz  10540  facp1  10709  facnn2  10713  faclbnd3  10722  bcn1  10737  hashfz0  10804  cvg1nlemres  10993  rexanuz  10996  fclim  11301  climmo  11305  iser3shft  11353  fsumsplitsn  11417  fsum2dlemstep  11441  fisumcom2  11445  arisum  11505  arisum2  11506  prodmodc  11585  fprodfac  11622  fprod2dlemstep  11629  fprodcom2fi  11633  fprodsplitsn  11640  eftlub  11697  ef01bndlem  11763  sin01gt0  11768  cos01gt0  11769  sin02gt0  11770  dvdsdivcl  11855  addmodlteqALT  11864  odd2np1  11877  oddge22np1  11885  m1expe  11903  nn0enne  11906  nn0o1gt2  11909  nno  11910  ndvdsadd  11935  infssuzcldc  11951  dfgcd2  12014  mulgcd  12016  algfx  12051  prmind2  12119  prm2orodd  12125  prmgt1  12131  oddprmgt2  12133  dfphi2  12219  nnnn0modprm0  12254  prm23lt5  12262  pythagtriplem2  12265  pcz  12330  dvdsprmpweqnn  12334  oddprmdvds  12351  prmunb  12359  4sqlem4  12389  evenennn  12393  dfgrp3me  12969  dvdsrcl2  13266  unitinvcl  13290  unitinvinv  13291  unitlinv  13293  unitrinv  13294  distop  13555  ntrss  13589  ssntr  13592  lmrcl  13661  lmreltop  13663  txuni2  13726  txcn  13745  hmeocnvb  13788  xmetunirn  13828  blssioo  14015  divcnap  14025  cdivcncfap  14057  dedekindeulemlub  14068  dedekindicclemlub  14077  dvexp2  14146  pilem3  14174  sincosq1sgn  14217  sincosq2sgn  14218  sincosq3sgn  14219  sincosq4sgn  14220  sinq12gt0  14221  zabsle1  14370  lgsdir2lem4  14402  2lgsoddprmlem3  14429  2sqlem2  14432  2sqlem10  14442  bj-pm2.18st  14472  bj-dcstab  14478  decidi  14517  sumdc2  14521  bj-charfunbi  14533  bdel  14567  bdssex  14624  bj-indind  14654  findset  14667  nninfall  14728  trirec0  14762  neap0mkv  14786