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  1396  xorbin  1403  xordc1  1412  biassdc  1414  nfr  1540  nfand  1590  19.21t  1604  19.30dc  1649  exintrbi  1655  19.9t  1664  nfnt  1678  equveli  1781  exdistrfor  1822  sbcof2  1832  sbidm  1873  sbi1v  1914  sbalyz  2026  sbal1yz  2028  nfsb4t  2041  euex  2083  eumo0  2084  mor  2095  exmodc  2103  mo3h  2106  mopick  2131  moexexdc  2137  euexex  2138  2euex  2140  exists2  2150  eqcoms  2207  eleq2s  2299  nfcr  2339  necon3ai  2424  rexnalim  2494  dfrex2dc  2496  rexex  2551  rsp  2552  ralim  2564  rexim  2599  r19.32r  2651  r19.44av  2664  r19.45av  2665  gencl  2803  gencbvex  2818  gencbval  2820  vtoclgf  2830  vtoclg1f  2831  pm13.183  2910  elrabi  2925  eueq2dc  2945  eueq3dc  2946  mob2  2952  euxfr2dc  2957  reu3  2962  rmoim  2973  2rmorex  2978  sbcex  3006  sbcbi2  3048  ra5  3086  sseq1  3215  difdif  3297  dfss4st  3405  difindiss  3426  undif3ss  3433  dfrab3ss  3450  abvor0dc  3483  reldisj  3511  disjel  3514  inssdif0im  3527  uneqdifeqim  3545  r19.2m  3546  r19.2mOLD  3547  r19.3rm  3548  r19.9rmv  3551  rexm  3559  ralm  3563  raaanlem  3564  ifnefalse  3581  ifnotdc  3608  ifandc  3609  ifmdc  3611  nelpri  3656  nelprd  3658  prprc1  3740  difprsn2  3772  diftpsn3  3773  snsssn  3801  preqr2  3809  preq12b  3810  opthpr  3812  prneimg  3814  oprcl  3842  pwprss  3845  intmin4  3912  uniintabim  3921  dfiin2g  3959  iinss2  3979  iundif2ss  3992  disjnim  4034  disjnims  4035  invdisj  4037  disjiun  4038  brne0  4092  brm  4093  trel  4148  trss  4150  ssex  4180  bnd2  4216  abssexg  4225  exmidexmid  4239  rext  4258  unipw  4260  euabex  4268  mss  4269  exss  4270  copsexg  4287  opelopabsb  4305  pwssunim  4330  epelg  4336  sowlin  4366  sotritric  4370  elsuci  4449  sucprc  4458  reusv3  4506  ordon  4533  onsucmin  4554  onsucelsucr  4555  unon  4558  onsucelsucexmid  4577  setind  4586  setind2  4587  sucprcreg  4596  en2lp  4601  eunex  4608  ordsoexmid  4609  ordpwsucss  4614  tfi  4629  peano1  4641  peano2  4642  find  4646  0nelelxp  4703  opelxp  4704  elvvuni  4738  optocl  4750  ralxpf  4823  rexxpf  4824  relop  4827  breldm  4881  dmxpm  4897  elreldm  4903  dmrnssfld  4940  dmcosseq  4949  resabs1  4987  resima2  4992  issref  5064  asymref  5067  xpidtr  5072  trin2  5073  poirr2  5074  xpmlem  5102  dmxpss  5112  xp11m  5120  cnveqb  5137  dfco2a  5182  cores2  5194  coi2  5198  relcnvtr  5201  relresfld  5211  relcnvexb  5221  cnviinm  5223  iotauni  5243  iota1  5245  iota4  5250  iotam  5262  dffun8  5298  fununfun  5316  funcnvsn  5318  imadif  5353  imainlem  5354  fcoi1  5455  fcoi2  5456  f0rn0  5469  f1ocnv  5534  f1ocnvb  5535  fun11iun  5542  ffoss  5553  f1o00  5556  fo00  5557  relelfvdm  5607  nfvres  5609  nfunsn  5610  ssimaex  5639  fvmptss2  5653  fvmptssdm  5663  unpreima  5704  respreima  5707  elrnrexdm  5718  elrnrexdmb  5719  rexrnmpt  5722  dffo4  5727  rnmptss  5740  funiun  5760  funopdmsn  5763  fvpr1  5787  fvpr2  5788  elunirn  5834  f1veqaeq  5837  isores1  5882  iotaexel  5903  riotauni  5905  riotacl2  5912  riota1  5917  riota1a  5918  snriota  5928  eusvobj2  5929  acexmidlema  5934  acexmidlemb  5935  acexmidlem2  5940  oprabid  5975  0neqopab  5989  brabvv  5990  1stval2  6240  2ndval2  6241  xp1st  6250  xp2nd  6251  unielxp  6259  releldm2  6270  cnvf1o  6310  fo2ndf  6312  poxp  6317  reldmtpos  6338  dftpos4  6348  tpostpos  6349  tpostpos2  6350  iunon  6369  smoel  6385  tfrlem4  6398  tfrlem7  6402  tfrlem8  6403  tfrlem9  6404  nnaord  6594  ecexr  6624  swoord1  6648  swoord2  6649  0er  6653  mapprc  6738  mapsnconst  6780  ixpf  6806  mptelixpg  6820  idssen  6867  ener  6870  en0  6886  en1  6890  en1bg  6891  2dom  6896  enm  6914  xpsnen  6915  ssenen  6947  snnen2og  6955  php5dom  6959  phpm  6961  findcard  6984  findcard2  6985  findcard2s  6986  unfiexmid  7014  fiintim  7027  fidcenumlemim  7053  sbthlem1  7058  fiss  7078  djuexb  7145  djuss  7171  eldju2ndl  7173  eldju2ndr  7174  ctssdclemr  7213  exmidlpo  7244  finnum  7289  ficardon  7295  exmidfodomrlemim  7308  acnrcl  7312  3nsssucpw1  7347  indpi  7454  subhalfnqq  7526  archnqq  7529  enq0sym  7544  nqnq0pi  7550  nqnq0  7553  mulnnnq0  7562  prml  7589  prmu  7590  prssnql  7591  prssnqu  7592  prcdnql  7596  prcunqu  7597  prltlu  7599  prnmaxl  7600  prnminu  7601  prloc  7603  prdisj  7604  addcanprg  7728  recexprlemopl  7737  recexprlemopu  7739  cauappcvgprlemladdfu  7766  caucvgprlemladdfu  7789  recexgt0sr  7885  renfdisj  8131  axsuploc  8144  negf1o  8453  recexre  8650  apsqgt0  8673  apreim  8675  aprcl  8718  recexaplem2  8724  rerecclap  8802  nn0ge0  9319  elnnnn0b  9338  xnn0xr  9362  xnn0nemnf  9368  xnn0nnn0pnf  9370  znegcl  9402  zeo  9477  nn0ind  9486  nn0ind-raph  9489  uzn0  9663  eluzaddi  9674  eluzsubi  9675  uznn0sub  9679  uz3m2nn  9693  uznnssnn  9697  uz2m1nn  9725  uz2mulcl  9728  indstr2  9729  qmulz  9743  qre  9745  qnegcl  9756  qreccl  9762  rphalflt  9804  nn0ledivnn  9888  xrltnr  9900  nltpnft  9935  ngtmnft  9938  xrrebnd  9940  xnegcl  9953  xnegneg  9954  xltnegi  9956  xrpnfdc  9963  xrmnfdc  9964  xnegid  9980  xaddid1  9983  xnn0lenn0nn0  9986  xnn0xadd0  9988  xposdif  10003  elioore  10033  elfzuz2  10150  uzsubsubfz  10168  fzdisj  10173  fzmmmeqm  10179  elfz0ubfz0  10246  elfz0fzfz0  10247  fz0fzelfz0  10248  fz0fzdiffz0  10251  elfzmlbp  10253  difelfzle  10255  difelfznle  10256  nn0disj  10259  2ffzeq  10262  fzo1fzo0n0  10305  elfzo0z  10306  elfzo0le  10307  fzonmapblen  10309  fzofzim  10310  elfzodifsumelfzo  10328  elfzonlteqm1  10337  fzonn0p1p1  10340  elfzom1p1elfzo  10341  ssfzo12bi  10352  ubmelm1fzo  10353  fzind2  10366  subfzo0  10369  infssuzcldc  10376  rebtwn2z  10395  fldiv4p1lem1div2  10446  fldiv4lem1div2  10448  flqeqceilz  10461  zmodidfzoimp  10497  modfzo0difsn  10538  nnsinds  10588  nn0sinds  10589  expcl2lemap  10694  qexpclz  10703  zzlesq  10851  facp1  10873  facnn2  10877  faclbnd3  10886  bcn1  10901  hashfz0  10968  wrdf  10998  cvg1nlemres  11238  rexanuz  11241  fclim  11547  climmo  11551  iser3shft  11599  fsumsplitsn  11663  fsum2dlemstep  11687  fisumcom2  11691  arisum  11751  arisum2  11752  prodmodc  11831  fprodfac  11868  fprod2dlemstep  11875  fprodcom2fi  11879  fprodsplitsn  11886  eftlub  11943  ef01bndlem  12009  sin01gt0  12015  cos01gt0  12016  sin02gt0  12017  dvdsdivcl  12103  addmodlteqALT  12112  odd2np1  12126  oddge22np1  12134  m1expe  12152  nn0enne  12155  nn0o1gt2  12158  nno  12159  ndvdsadd  12184  dfgcd2  12277  mulgcd  12279  algfx  12316  prmind2  12384  prm2orodd  12390  prmgt1  12396  oddprmgt2  12398  dfphi2  12484  nnnn0modprm0  12520  prm23lt5  12528  pythagtriplem2  12531  pcz  12597  dvdsprmpweqnn  12601  oddprmdvds  12619  prmunb  12627  4sqlem4  12657  4sqlem19  12674  evenennn  12706  fngsum  13162  igsumvalx  13163  dfgrp3me  13374  mulgnn0gsum  13406  rngdi  13644  rngdir  13645  dvdsrcl2  13803  unitinvcl  13827  unitinvinv  13828  unitlinv  13830  unitrinv  13831  rmodislmodlem  14054  rmodislmod  14055  zrhval  14321  psrbagf  14374  distop  14499  ntrss  14533  ssntr  14536  lmrcl  14605  lmreltop  14607  txuni2  14670  txcn  14689  hmeocnvb  14732  xmetunirn  14772  blssioo  14967  divcnap  14979  cdivcncfap  15018  dedekindeulemlub  15034  dedekindicclemlub  15043  dvexp2  15126  elply2  15149  plyco  15173  pilem3  15197  sincosq1sgn  15240  sincosq2sgn  15241  sincosq3sgn  15242  sincosq4sgn  15243  sinq12gt0  15244  fsumdvdsmul  15405  zabsle1  15418  lgsdir2lem4  15450  gausslemma2dlem0f  15473  gausslemma2dlem1a  15477  gausslemma2dlem2  15481  gausslemma2dlem3  15482  gausslemma2dlem4  15483  2lgslem1a1  15505  2lgslem3  15520  2lgsoddprmlem3  15530  2lgsoddprm  15532  2sqlem2  15534  2sqlem10  15544  bj-pm2.18st  15619  bj-dcstab  15625  decidi  15664  sumdc2  15668  bj-charfunbi  15680  bdel  15714  bdssex  15771  bj-indind  15801  findset  15814  nninfall  15879  trirec0  15916  neap0mkv  15941