Theorem sylbi 120

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 119	. 2 |- ( ph -> ps )
3		sylbi.2	. 2 |- ( ps -> ch )
4	2, 3	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbb  122  sylbb2  137  3imtr4i  200  simplbiim  384  mpan10  465  an12s  554  an32s  557  an4s  577  sylnbi  667  dcim  826  notnotrdc  828  const  837  condcOLD  839  pm2.61ddc  846  pm5.18dc  868  pm2.25dc  878  pm2.85dc  890  pm5.12dc  895  pm5.14dc  896  pm5.55dc  898  peircedc  899  pm5.54dc  903  dcor  919  pm5.62dc  929  pm5.63dc  930  pm4.83dc  935  3simpb  979  3simpc  980  3imp  1175  3com12  1185  3com13  1186  syl3anb  1259  xoranor  1355  xorbin  1362  xordc1  1371  biassdc  1373  nfr  1498  nfand  1547  19.21t  1561  19.30dc  1606  exintrbi  1612  19.9t  1621  nfnt  1634  equveli  1732  exdistrfor  1772  sbcof2  1782  sbidm  1823  sbi1v  1863  sbalyz  1974  sbal1yz  1976  nfsb4t  1989  euex  2029  eumo0  2030  mor  2041  exmodc  2049  mo3h  2052  mopick  2077  moexexdc  2083  euexex  2084  2euex  2086  exists2  2096  eqcoms  2142  eleq2s  2234  nfcr  2273  necon3ai  2357  rexnalim  2427  dfrex2dc  2428  rexex  2479  rsp  2480  ralim  2491  rexim  2526  r19.32r  2578  r19.44av  2590  r19.45av  2591  gencl  2718  gencbvex  2732  gencbval  2734  vtoclgf  2744  vtoclg1f  2745  pm13.183  2822  elrabi  2837  eueq2dc  2857  eueq3dc  2858  mob2  2864  euxfr2dc  2869  reu3  2874  rmoim  2885  2rmorex  2890  sbcex  2917  sbcbi2  2959  ra5  2997  sseq1  3120  difdif  3201  dfss4st  3309  difindiss  3330  undif3ss  3337  dfrab3ss  3354  abvor0dc  3386  reldisj  3414  disjel  3417  inssdif0im  3430  uneqdifeqim  3448  r19.2m  3449  r19.2mOLD  3450  r19.3rm  3451  r19.9rmv  3454  rexm  3462  ralm  3467  raaanlem  3468  ifnefalse  3485  ifandc  3508  ifmdc  3509  nelpri  3551  nelprd  3553  prprc1  3631  difprsn2  3660  diftpsn3  3661  snsssn  3688  preqr2  3696  preq12b  3697  opthpr  3699  prneimg  3701  oprcl  3729  pwprss  3732  intmin4  3799  uniintabim  3808  dfiin2g  3846  iinss2  3865  iundif2ss  3878  disjnim  3920  disjnims  3921  invdisj  3923  disjiun  3924  brne0  3977  brm  3978  trel  4033  trss  4035  ssex  4065  bnd2  4097  abssexg  4106  exmidexmid  4120  rext  4137  unipw  4139  euabex  4147  mss  4148  exss  4149  copsexg  4166  opelopabsb  4182  pwssunim  4206  epelg  4212  sowlin  4242  sotritric  4246  elsuci  4325  sucprc  4334  reusv3  4381  ordon  4402  onsucmin  4423  onsucelsucr  4424  unon  4427  onsucelsucexmid  4445  setind  4454  setind2  4455  sucprcreg  4464  en2lp  4469  eunex  4476  ordsoexmid  4477  ordpwsucss  4482  tfi  4496  peano1  4508  peano2  4509  find  4513  0nelelxp  4568  opelxp  4569  elvvuni  4603  optocl  4615  ralxpf  4685  rexxpf  4686  relop  4689  breldm  4743  dmxpm  4759  elreldm  4765  dmrnssfld  4802  dmcosseq  4810  resabs1  4848  resima2  4853  issref  4921  asymref  4924  xpidtr  4929  trin2  4930  poirr2  4931  xpmlem  4959  dmxpss  4969  xp11m  4977  cnveqb  4994  dfco2a  5039  cores2  5051  coi2  5055  relcnvtr  5058  relresfld  5068  relcnvexb  5078  cnviinm  5080  iotauni  5100  iota1  5102  iota4  5106  dffun8  5151  funcnvsn  5168  imadif  5203  imainlem  5204  fcoi1  5303  fcoi2  5304  f0rn0  5317  f1ocnv  5380  f1ocnvb  5381  fun11iun  5388  ffoss  5399  f1o00  5402  fo00  5403  relelfvdm  5453  nfvres  5454  nfunsn  5455  ssimaex  5482  fvmptss2  5496  fvmptssdm  5505  unpreima  5545  respreima  5548  elrnrexdm  5559  elrnrexdmb  5560  rexrnmpt  5563  dffo4  5568  rnmptss  5581  fvpr1  5624  fvpr2  5625  elunirn  5667  f1veqaeq  5670  isores1  5715  riotauni  5736  riotacl2  5743  riota1  5748  riota1a  5749  snriota  5759  eusvobj2  5760  acexmidlema  5765  acexmidlemb  5766  acexmidlem2  5771  oprabid  5803  0neqopab  5816  brabvv  5817  1stval2  6053  2ndval2  6054  xp1st  6063  xp2nd  6064  unielxp  6072  releldm2  6083  cnvf1o  6122  fo2ndf  6124  poxp  6129  reldmtpos  6150  dftpos4  6160  tpostpos  6161  tpostpos2  6162  iunon  6181  smoel  6197  tfrlem4  6210  tfrlem7  6214  tfrlem8  6215  tfrlem9  6216  nnaord  6405  ecexr  6434  swoord1  6458  swoord2  6459  0er  6463  mapprc  6546  mapsnconst  6588  ixpf  6614  mptelixpg  6628  idssen  6671  ener  6673  en0  6689  en1  6693  en1bg  6694  2dom  6699  enm  6714  xpsnen  6715  ssenen  6745  snnen2og  6753  php5dom  6757  phpm  6759  findcard  6782  findcard2  6783  findcard2s  6784  unfiexmid  6806  fiintim  6817  fidcenumlemim  6840  sbthlem1  6845  fiss  6865  djuexb  6929  djuss  6955  eldju2ndl  6957  eldju2ndr  6958  ctssdclemr  6997  exmidlpo  7015  finnum  7039  exmidfodomrlemim  7057  indpi  7150  subhalfnqq  7222  archnqq  7225  enq0sym  7240  nqnq0pi  7246  nqnq0  7249  mulnnnq0  7258  prml  7285  prmu  7286  prssnql  7287  prssnqu  7288  prcdnql  7292  prcunqu  7293  prltlu  7295  prnmaxl  7296  prnminu  7297  prloc  7299  prdisj  7300  addcanprg  7424  recexprlemopl  7433  recexprlemopu  7435  cauappcvgprlemladdfu  7462  caucvgprlemladdfu  7485  recexgt0sr  7581  renfdisj  7824  axsuploc  7837  negf1o  8144  recexre  8340  apsqgt0  8363  apreim  8365  aprcl  8408  recexaplem2  8413  rerecclap  8490  nn0ge0  9002  elnnnn0b  9021  xnn0xr  9045  xnn0nemnf  9051  xnn0nnn0pnf  9053  znegcl  9085  zeo  9156  nn0ind  9165  nn0ind-raph  9168  uzn0  9341  eluzaddi  9352  eluzsubi  9353  uznn0sub  9357  uz3m2nn  9368  uznnssnn  9372  uz2m1nn  9399  uz2mulcl  9402  indstr2  9403  qmulz  9415  qre  9417  qnegcl  9428  qreccl  9434  rphalflt  9471  nn0ledivnn  9554  xrltnr  9566  nltpnft  9597  ngtmnft  9600  xrrebnd  9602  xnegcl  9615  xnegneg  9616  xltnegi  9618  xrpnfdc  9625  xrmnfdc  9626  xnegid  9642  xaddid1  9645  xnn0lenn0nn0  9648  xnn0xadd0  9650  xposdif  9665  elioore  9695  elfzuz2  9809  uzsubsubfz  9827  fzdisj  9832  fzmmmeqm  9838  elfz0ubfz0  9902  elfz0fzfz0  9903  fz0fzelfz0  9904  fz0fzdiffz0  9907  elfzmlbp  9909  difelfzle  9911  difelfznle  9912  nn0disj  9915  2ffzeq  9918  fzo1fzo0n0  9960  elfzo0z  9961  elfzo0le  9962  fzonmapblen  9964  fzofzim  9965  elfzodifsumelfzo  9978  elfzonlteqm1  9987  fzonn0p1p1  9990  elfzom1p1elfzo  9991  ssfzo12bi  10002  ubmelm1fzo  10003  fzind2  10016  subfzo0  10019  rebtwn2z  10032  fldiv4p1lem1div2  10078  flqeqceilz  10091  zmodidfzoimp  10127  modfzo0difsn  10168  nnsinds  10216  nn0sinds  10217  expcl2lemap  10305  qexpclz  10314  facp1  10476  facnn2  10480  faclbnd3  10489  bcn1  10504  hashfz0  10571  cvg1nlemres  10757  rexanuz  10760  fclim  11063  climmo  11067  iser3shft  11115  fsumsplitsn  11179  fsum2dlemstep  11203  fisumcom2  11207  arisum  11267  arisum2  11268  prodmodc  11347  eftlub  11396  ef01bndlem  11463  sin01gt0  11468  cos01gt0  11469  sin02gt0  11470  dvdsdivcl  11548  addmodlteqALT  11557  odd2np1  11570  oddge22np1  11578  m1expe  11596  nn0enne  11599  nn0o1gt2  11602  nno  11603  ndvdsadd  11628  infssuzcldc  11644  dfgcd2  11702  mulgcd  11704  algfx  11733  prmind2  11801  prm2orodd  11807  prmgt1  11812  oddprmgt2  11814  dfphi2  11896  evenennn  11906  distop  12254  ntrss  12288  ssntr  12291  lmrcl  12360  lmreltop  12362  txuni2  12425  txcn  12444  hmeocnvb  12487  xmetunirn  12527  blssioo  12714  divcnap  12724  cdivcncfap  12756  dedekindeulemlub  12767  dedekindicclemlub  12776  dvexp2  12845  pilem3  12864  sincosq1sgn  12907  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  sinq12gt0  12911  bj-pm2.18st  12958  bj-dcstab  12961  decidi  13002  sumdc2  13006  bdel  13043  bdssex  13100  bj-indind  13130  findset  13143  nninfall  13204