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  2770  gencbvex  2784  gencbval  2786  vtoclgf  2796  vtoclg1f  2797  pm13.183  2876  elrabi  2891  eueq2dc  2911  eueq3dc  2912  mob2  2918  euxfr2dc  2923  reu3  2928  rmoim  2939  2rmorex  2944  sbcex  2972  sbcbi2  3014  ra5  3052  sseq1  3179  difdif  3261  dfss4st  3369  difindiss  3390  undif3ss  3397  dfrab3ss  3414  abvor0dc  3447  reldisj  3475  disjel  3478  inssdif0im  3491  uneqdifeqim  3509  r19.2m  3510  r19.2mOLD  3511  r19.3rm  3512  r19.9rmv  3515  rexm  3523  ralm  3528  raaanlem  3529  ifnefalse  3546  ifnotdc  3572  ifandc  3573  ifmdc  3575  nelpri  3617  nelprd  3619  prprc1  3701  difprsn2  3733  diftpsn3  3734  snsssn  3762  preqr2  3770  preq12b  3771  opthpr  3773  prneimg  3775  oprcl  3803  pwprss  3806  intmin4  3873  uniintabim  3882  dfiin2g  3920  iinss2  3940  iundif2ss  3953  disjnim  3995  disjnims  3996  invdisj  3998  disjiun  3999  brne0  4053  brm  4054  trel  4109  trss  4111  ssex  4141  bnd2  4174  abssexg  4183  exmidexmid  4197  rext  4216  unipw  4218  euabex  4226  mss  4227  exss  4228  copsexg  4245  opelopabsb  4261  pwssunim  4285  epelg  4291  sowlin  4321  sotritric  4325  elsuci  4404  sucprc  4413  reusv3  4461  ordon  4486  onsucmin  4507  onsucelsucr  4508  unon  4511  onsucelsucexmid  4530  setind  4539  setind2  4540  sucprcreg  4549  en2lp  4554  eunex  4561  ordsoexmid  4562  ordpwsucss  4567  tfi  4582  peano1  4594  peano2  4595  find  4599  0nelelxp  4656  opelxp  4657  elvvuni  4691  optocl  4703  ralxpf  4774  rexxpf  4775  relop  4778  breldm  4832  dmxpm  4848  elreldm  4854  dmrnssfld  4891  dmcosseq  4899  resabs1  4937  resima2  4942  issref  5012  asymref  5015  xpidtr  5020  trin2  5021  poirr2  5022  xpmlem  5050  dmxpss  5060  xp11m  5068  cnveqb  5085  dfco2a  5130  cores2  5142  coi2  5146  relcnvtr  5149  relresfld  5159  relcnvexb  5169  cnviinm  5171  iotauni  5191  iota1  5193  iota4  5197  iotam  5209  dffun8  5245  funcnvsn  5262  imadif  5297  imainlem  5298  fcoi1  5397  fcoi2  5398  f0rn0  5411  f1ocnv  5475  f1ocnvb  5476  fun11iun  5483  ffoss  5494  f1o00  5497  fo00  5498  relelfvdm  5548  nfvres  5549  nfunsn  5550  ssimaex  5578  fvmptss2  5592  fvmptssdm  5601  unpreima  5642  respreima  5645  elrnrexdm  5656  elrnrexdmb  5657  rexrnmpt  5660  dffo4  5665  rnmptss  5678  fvpr1  5721  fvpr2  5722  elunirn  5767  f1veqaeq  5770  isores1  5815  riotauni  5837  riotacl2  5844  riota1  5849  riota1a  5850  snriota  5860  eusvobj2  5861  acexmidlema  5866  acexmidlemb  5867  acexmidlem2  5872  oprabid  5907  0neqopab  5920  brabvv  5921  1stval2  6156  2ndval2  6157  xp1st  6166  xp2nd  6167  unielxp  6175  releldm2  6186  cnvf1o  6226  fo2ndf  6228  poxp  6233  reldmtpos  6254  dftpos4  6264  tpostpos  6265  tpostpos2  6266  iunon  6285  smoel  6301  tfrlem4  6314  tfrlem7  6318  tfrlem8  6319  tfrlem9  6320  nnaord  6510  ecexr  6540  swoord1  6564  swoord2  6565  0er  6569  mapprc  6652  mapsnconst  6694  ixpf  6720  mptelixpg  6734  idssen  6777  ener  6779  en0  6795  en1  6799  en1bg  6800  2dom  6805  enm  6820  xpsnen  6821  ssenen  6851  snnen2og  6859  php5dom  6863  phpm  6865  findcard  6888  findcard2  6889  findcard2s  6890  unfiexmid  6917  fiintim  6928  fidcenumlemim  6951  sbthlem1  6956  fiss  6976  djuexb  7043  djuss  7069  eldju2ndl  7071  eldju2ndr  7072  ctssdclemr  7111  exmidlpo  7141  finnum  7182  exmidfodomrlemim  7200  3nsssucpw1  7235  indpi  7341  subhalfnqq  7413  archnqq  7416  enq0sym  7431  nqnq0pi  7437  nqnq0  7440  mulnnnq0  7449  prml  7476  prmu  7477  prssnql  7478  prssnqu  7479  prcdnql  7483  prcunqu  7484  prltlu  7486  prnmaxl  7487  prnminu  7488  prloc  7490  prdisj  7491  addcanprg  7615  recexprlemopl  7624  recexprlemopu  7626  cauappcvgprlemladdfu  7653  caucvgprlemladdfu  7676  recexgt0sr  7772  renfdisj  8017  axsuploc  8030  negf1o  8339  recexre  8535  apsqgt0  8558  apreim  8560  aprcl  8603  recexaplem2  8609  rerecclap  8687  nn0ge0  9201  elnnnn0b  9220  xnn0xr  9244  xnn0nemnf  9250  xnn0nnn0pnf  9252  znegcl  9284  zeo  9358  nn0ind  9367  nn0ind-raph  9370  uzn0  9543  eluzaddi  9554  eluzsubi  9555  uznn0sub  9559  uz3m2nn  9573  uznnssnn  9577  uz2m1nn  9605  uz2mulcl  9608  indstr2  9609  qmulz  9623  qre  9625  qnegcl  9636  qreccl  9642  rphalflt  9683  nn0ledivnn  9767  xrltnr  9779  nltpnft  9814  ngtmnft  9817  xrrebnd  9819  xnegcl  9832  xnegneg  9833  xltnegi  9835  xrpnfdc  9842  xrmnfdc  9843  xnegid  9859  xaddid1  9862  xnn0lenn0nn0  9865  xnn0xadd0  9867  xposdif  9882  elioore  9912  elfzuz2  10029  uzsubsubfz  10047  fzdisj  10052  fzmmmeqm  10058  elfz0ubfz0  10125  elfz0fzfz0  10126  fz0fzelfz0  10127  fz0fzdiffz0  10130  elfzmlbp  10132  difelfzle  10134  difelfznle  10135  nn0disj  10138  2ffzeq  10141  fzo1fzo0n0  10183  elfzo0z  10184  elfzo0le  10185  fzonmapblen  10187  fzofzim  10188  elfzodifsumelfzo  10201  elfzonlteqm1  10210  fzonn0p1p1  10213  elfzom1p1elfzo  10214  ssfzo12bi  10225  ubmelm1fzo  10226  fzind2  10239  subfzo0  10242  rebtwn2z  10255  fldiv4p1lem1div2  10305  flqeqceilz  10318  zmodidfzoimp  10354  modfzo0difsn  10395  nnsinds  10443  nn0sinds  10444  expcl2lemap  10532  qexpclz  10541  facp1  10710  facnn2  10714  faclbnd3  10723  bcn1  10738  hashfz0  10805  cvg1nlemres  10994  rexanuz  10997  fclim  11302  climmo  11306  iser3shft  11354  fsumsplitsn  11418  fsum2dlemstep  11442  fisumcom2  11446  arisum  11506  arisum2  11507  prodmodc  11586  fprodfac  11623  fprod2dlemstep  11630  fprodcom2fi  11634  fprodsplitsn  11641  eftlub  11698  ef01bndlem  11764  sin01gt0  11769  cos01gt0  11770  sin02gt0  11771  dvdsdivcl  11856  addmodlteqALT  11865  odd2np1  11878  oddge22np1  11886  m1expe  11904  nn0enne  11907  nn0o1gt2  11910  nno  11911  ndvdsadd  11936  infssuzcldc  11952  dfgcd2  12015  mulgcd  12017  algfx  12052  prmind2  12120  prm2orodd  12126  prmgt1  12132  oddprmgt2  12134  dfphi2  12220  nnnn0modprm0  12255  prm23lt5  12263  pythagtriplem2  12266  pcz  12331  dvdsprmpweqnn  12335  oddprmdvds  12352  prmunb  12360  4sqlem4  12390  evenennn  12394  dfgrp3me  12970  dvdsrcl2  13268  unitinvcl  13292  unitinvinv  13293  unitlinv  13295  unitrinv  13296  rmodislmodlem  13440  rmodislmod  13441  distop  13588  ntrss  13622  ssntr  13625  lmrcl  13694  lmreltop  13696  txuni2  13759  txcn  13778  hmeocnvb  13821  xmetunirn  13861  blssioo  14048  divcnap  14058  cdivcncfap  14090  dedekindeulemlub  14101  dedekindicclemlub  14110  dvexp2  14179  pilem3  14207  sincosq1sgn  14250  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  sinq12gt0  14254  zabsle1  14403  lgsdir2lem4  14435  2lgsoddprmlem3  14462  2sqlem2  14465  2sqlem10  14475  bj-pm2.18st  14505  bj-dcstab  14511  decidi  14550  sumdc2  14554  bj-charfunbi  14566  bdel  14600  bdssex  14657  bj-indind  14687  findset  14700  nninfall  14761  trirec0  14795  neap0mkv  14819