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  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  2015  sbal1yz  2017  nfsb4t  2030  euex  2072  eumo0  2073  mor  2084  exmodc  2092  mo3h  2095  mopick  2120  moexexdc  2126  euexex  2127  2euex  2129  exists2  2139  eqcoms  2196  eleq2s  2288  nfcr  2328  necon3ai  2413  rexnalim  2483  dfrex2dc  2485  rexex  2540  rsp  2541  ralim  2553  rexim  2588  r19.32r  2640  r19.44av  2653  r19.45av  2654  gencl  2792  gencbvex  2807  gencbval  2809  vtoclgf  2819  vtoclg1f  2820  pm13.183  2899  elrabi  2914  eueq2dc  2934  eueq3dc  2935  mob2  2941  euxfr2dc  2946  reu3  2951  rmoim  2962  2rmorex  2967  sbcex  2995  sbcbi2  3037  ra5  3075  sseq1  3203  difdif  3285  dfss4st  3393  difindiss  3414  undif3ss  3421  dfrab3ss  3438  abvor0dc  3471  reldisj  3499  disjel  3502  inssdif0im  3515  uneqdifeqim  3533  r19.2m  3534  r19.2mOLD  3535  r19.3rm  3536  r19.9rmv  3539  rexm  3547  ralm  3551  raaanlem  3552  ifnefalse  3569  ifnotdc  3595  ifandc  3596  ifmdc  3598  nelpri  3643  nelprd  3645  prprc1  3727  difprsn2  3759  diftpsn3  3760  snsssn  3788  preqr2  3796  preq12b  3797  opthpr  3799  prneimg  3801  oprcl  3829  pwprss  3832  intmin4  3899  uniintabim  3908  dfiin2g  3946  iinss2  3966  iundif2ss  3979  disjnim  4021  disjnims  4022  invdisj  4024  disjiun  4025  brne0  4079  brm  4080  trel  4135  trss  4137  ssex  4167  bnd2  4203  abssexg  4212  exmidexmid  4226  rext  4245  unipw  4247  euabex  4255  mss  4256  exss  4257  copsexg  4274  opelopabsb  4291  pwssunim  4316  epelg  4322  sowlin  4352  sotritric  4356  elsuci  4435  sucprc  4444  reusv3  4492  ordon  4519  onsucmin  4540  onsucelsucr  4541  unon  4544  onsucelsucexmid  4563  setind  4572  setind2  4573  sucprcreg  4582  en2lp  4587  eunex  4594  ordsoexmid  4595  ordpwsucss  4600  tfi  4615  peano1  4627  peano2  4628  find  4632  0nelelxp  4689  opelxp  4690  elvvuni  4724  optocl  4736  ralxpf  4809  rexxpf  4810  relop  4813  breldm  4867  dmxpm  4883  elreldm  4889  dmrnssfld  4926  dmcosseq  4934  resabs1  4972  resima2  4977  issref  5049  asymref  5052  xpidtr  5057  trin2  5058  poirr2  5059  xpmlem  5087  dmxpss  5097  xp11m  5105  cnveqb  5122  dfco2a  5167  cores2  5179  coi2  5183  relcnvtr  5186  relresfld  5196  relcnvexb  5206  cnviinm  5208  iotauni  5228  iota1  5230  iota4  5235  iotam  5247  dffun8  5283  funcnvsn  5300  imadif  5335  imainlem  5336  fcoi1  5435  fcoi2  5436  f0rn0  5449  f1ocnv  5514  f1ocnvb  5515  fun11iun  5522  ffoss  5533  f1o00  5536  fo00  5537  relelfvdm  5587  nfvres  5589  nfunsn  5590  ssimaex  5619  fvmptss2  5633  fvmptssdm  5643  unpreima  5684  respreima  5687  elrnrexdm  5698  elrnrexdmb  5699  rexrnmpt  5702  dffo4  5707  rnmptss  5720  fvpr1  5763  fvpr2  5764  elunirn  5810  f1veqaeq  5813  isores1  5858  iotaexel  5879  riotauni  5881  riotacl2  5888  riota1  5893  riota1a  5894  snriota  5904  eusvobj2  5905  acexmidlema  5910  acexmidlemb  5911  acexmidlem2  5916  oprabid  5951  0neqopab  5964  brabvv  5965  1stval2  6210  2ndval2  6211  xp1st  6220  xp2nd  6221  unielxp  6229  releldm2  6240  cnvf1o  6280  fo2ndf  6282  poxp  6287  reldmtpos  6308  dftpos4  6318  tpostpos  6319  tpostpos2  6320  iunon  6339  smoel  6355  tfrlem4  6368  tfrlem7  6372  tfrlem8  6373  tfrlem9  6374  nnaord  6564  ecexr  6594  swoord1  6618  swoord2  6619  0er  6623  mapprc  6708  mapsnconst  6750  ixpf  6776  mptelixpg  6790  idssen  6833  ener  6835  en0  6851  en1  6855  en1bg  6856  2dom  6861  enm  6876  xpsnen  6877  ssenen  6909  snnen2og  6917  php5dom  6921  phpm  6923  findcard  6946  findcard2  6947  findcard2s  6948  unfiexmid  6976  fiintim  6987  fidcenumlemim  7013  sbthlem1  7018  fiss  7038  djuexb  7105  djuss  7131  eldju2ndl  7133  eldju2ndr  7134  ctssdclemr  7173  exmidlpo  7204  finnum  7245  exmidfodomrlemim  7263  3nsssucpw1  7298  indpi  7404  subhalfnqq  7476  archnqq  7479  enq0sym  7494  nqnq0pi  7500  nqnq0  7503  mulnnnq0  7512  prml  7539  prmu  7540  prssnql  7541  prssnqu  7542  prcdnql  7546  prcunqu  7547  prltlu  7549  prnmaxl  7550  prnminu  7551  prloc  7553  prdisj  7554  addcanprg  7678  recexprlemopl  7687  recexprlemopu  7689  cauappcvgprlemladdfu  7716  caucvgprlemladdfu  7739  recexgt0sr  7835  renfdisj  8081  axsuploc  8094  negf1o  8403  recexre  8599  apsqgt0  8622  apreim  8624  aprcl  8667  recexaplem2  8673  rerecclap  8751  nn0ge0  9268  elnnnn0b  9287  xnn0xr  9311  xnn0nemnf  9317  xnn0nnn0pnf  9319  znegcl  9351  zeo  9425  nn0ind  9434  nn0ind-raph  9437  uzn0  9611  eluzaddi  9622  eluzsubi  9623  uznn0sub  9627  uz3m2nn  9641  uznnssnn  9645  uz2m1nn  9673  uz2mulcl  9676  indstr2  9677  qmulz  9691  qre  9693  qnegcl  9704  qreccl  9710  rphalflt  9752  nn0ledivnn  9836  xrltnr  9848  nltpnft  9883  ngtmnft  9886  xrrebnd  9888  xnegcl  9901  xnegneg  9902  xltnegi  9904  xrpnfdc  9911  xrmnfdc  9912  xnegid  9928  xaddid1  9931  xnn0lenn0nn0  9934  xnn0xadd0  9936  xposdif  9951  elioore  9981  elfzuz2  10098  uzsubsubfz  10116  fzdisj  10121  fzmmmeqm  10127  elfz0ubfz0  10194  elfz0fzfz0  10195  fz0fzelfz0  10196  fz0fzdiffz0  10199  elfzmlbp  10201  difelfzle  10203  difelfznle  10204  nn0disj  10207  2ffzeq  10210  fzo1fzo0n0  10253  elfzo0z  10254  elfzo0le  10255  fzonmapblen  10257  fzofzim  10258  elfzodifsumelfzo  10271  elfzonlteqm1  10280  fzonn0p1p1  10283  elfzom1p1elfzo  10284  ssfzo12bi  10295  ubmelm1fzo  10296  fzind2  10309  subfzo0  10312  rebtwn2z  10326  fldiv4p1lem1div2  10377  fldiv4lem1div2  10379  flqeqceilz  10392  zmodidfzoimp  10428  modfzo0difsn  10469  nnsinds  10519  nn0sinds  10520  expcl2lemap  10625  qexpclz  10634  zzlesq  10782  facp1  10804  facnn2  10808  faclbnd3  10817  bcn1  10832  hashfz0  10899  wrdf  10923  cvg1nlemres  11132  rexanuz  11135  fclim  11440  climmo  11444  iser3shft  11492  fsumsplitsn  11556  fsum2dlemstep  11580  fisumcom2  11584  arisum  11644  arisum2  11645  prodmodc  11724  fprodfac  11761  fprod2dlemstep  11768  fprodcom2fi  11772  fprodsplitsn  11779  eftlub  11836  ef01bndlem  11902  sin01gt0  11908  cos01gt0  11909  sin02gt0  11910  dvdsdivcl  11995  addmodlteqALT  12004  odd2np1  12017  oddge22np1  12025  m1expe  12043  nn0enne  12046  nn0o1gt2  12049  nno  12050  ndvdsadd  12075  infssuzcldc  12091  dfgcd2  12154  mulgcd  12156  algfx  12193  prmind2  12261  prm2orodd  12267  prmgt1  12273  oddprmgt2  12275  dfphi2  12361  nnnn0modprm0  12396  prm23lt5  12404  pythagtriplem2  12407  pcz  12473  dvdsprmpweqnn  12477  oddprmdvds  12495  prmunb  12503  4sqlem4  12533  4sqlem19  12550  evenennn  12553  fngsum  12974  igsumvalx  12975  dfgrp3me  13175  mulgnn0gsum  13201  rngdi  13439  rngdir  13440  dvdsrcl2  13598  unitinvcl  13622  unitinvinv  13623  unitlinv  13625  unitrinv  13626  rmodislmodlem  13849  rmodislmod  13850  zrhval  14116  psrbagf  14167  distop  14264  ntrss  14298  ssntr  14301  lmrcl  14370  lmreltop  14372  txuni2  14435  txcn  14454  hmeocnvb  14497  xmetunirn  14537  blssioo  14732  divcnap  14744  cdivcncfap  14783  dedekindeulemlub  14799  dedekindicclemlub  14808  dvexp2  14891  elply2  14914  plyco  14937  pilem3  14959  sincosq1sgn  15002  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  zabsle1  15156  lgsdir2lem4  15188  gausslemma2dlem0f  15211  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  gausslemma2dlem3  15220  gausslemma2dlem4  15221  2lgslem1a1  15243  2lgslem3  15258  2lgsoddprmlem3  15268  2lgsoddprm  15270  2sqlem2  15272  2sqlem10  15282  bj-pm2.18st  15312  bj-dcstab  15318  decidi  15357  sumdc2  15361  bj-charfunbi  15373  bdel  15407  bdssex  15464  bj-indind  15494  findset  15507  nninfall  15569  trirec0  15604  neap0mkv  15629