Theorem sylbi 187

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 5-Aug-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 186	. 2 |- (ph -> ps)
3		sylbi.2	. 2 |- (ps -> ch)
4	2, 3	syl 15	1 |- (ph -> ch)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  bi2  189  3imtr4i  257  sylnbi  297  imp  418  an12s  776  an32s  779  an4s  799  oibabs  851  3simpb  953  3simpc  954  3imp  1145  3com12  1155  3com13  1156  syl3anb  1225  19.33b  1608  exintrbi  1613  ax17e  1618  spimfw  1646  a6e  1751  nfr  1761  19.9t  1779  nfnd  1791  nfndOLD  1792  equs5e  1888  exdistrf  1971  equvini  1987  equveli  1988  ax10-16  2190  euex  2227  eumo0  2228  mopick  2266  2euex  2276  2mo  2282  2eu3  2286  exists2  2294  eqcoms  2356  eleq2s  2445  nfcr  2482  necon3bi  2558  necon1ai  2559  necon2ai  2562  pm2.61ne  2592  pm2.61ine  2593  rexex  2674  rsp  2675  ralim  2686  r19.36av  2760  r19.37  2761  r19.44av  2768  r19.45av  2769  gencl  2888  gencbvex  2902  vtoclgf  2914  pm13.183  2980  mo2icl  3016  mob2  3017  reu3  3027  rmoim  3036  2reuswap  3039  sbcex  3056  ra5  3131  sseq1  3293  unineq  3506  dfrab3ss  3534  reldisj  3595  disjel  3598  pssdif  3613  difin0ss  3617  uneqdifeq  3639  r19.2z  3640  r19.3rz  3642  r19.3rzv  3644  ralidm  3654  ifnefalse  3671  ifbi  3680  nelpri  3755  difprsn2  3849  diftpsn3  3850  pwpw0  3856  ssunsn2  3866  snsssn  3874  pwsnALT  3883  intmin4  3956  dfiin2g  4001  iinss2  4019  unipw  4118  pwadjoin  4120  preqr2  4126  preq12b  4128  opkthg  4132  pw10  4162  pw10b  4167  pw1disj  4168  pw1ss  4170  sikss1c1c  4268  opkelimagekg  4272  ins2kss  4280  ins3kss  4281  cokrelk  4285  eqpw1uni  4331  pw1eqadj  4333  euabex  4335  iotauni  4352  iota1  4354  iota4  4358  reiotacl2  4364  dfiota4  4373  0nelsuc  4401  nndisjeq  4430  snfi  4432  lefinlteq  4464  ssfin  4471  tfinprop  4490  evenoddnnnul  4515  evenodddisj  4517  sfin112  4530  sfintfin  4533  sfinltfin  4536  sfin111  4537  spfinsfincl  4540  vfinspnn  4542  vfinspsslem1  4551  copsexg  4608  ralxpf  4828  optocl  4839  breldm  4912  proj1eldm  4928  dmcoss  4972  xpnz  5046  xp11  5057  xpcan  5058  xpcan2  5059  dfco2a  5082  cores2  5092  dfxp2  5114  dffun8  5135  fununi  5161  imadif  5172  fneu  5188  ffoss  5315  f1o00  5318  fo00  5319  nfunsn  5354  fvun1  5380  fvimacnv  5404  unpreima  5409  inpreima  5410  respreima  5411  fvpr1  5450  1stfo  5506  2ndfo  5507  xpnedisj  5514  1st2nd2  5517  oprabid  5551  oprssdm  5613  fvmptss  5706  fvmptss2  5726  op1st2nd  5791  oqelins4  5795  addcfnex  5825  pw1fnf1o  5856  clos1nrel  5887  weds  5939  ecexr  5951  mapprc  6005  mapsspm  6022  mapsspw  6023  map0b  6025  map0  6026  ensymi  6037  entr  6039  idssen  6041  en0  6043  fundmen  6044  xpen  6056  enpw1  6063  enmap2  6069  enmap1  6075  enprmaplem3  6079  nenpw1pwlem2  6086  ncseqnc  6129  muccl  6133  muccom  6135  mucass  6136  1cnc  6140  muc0  6143  mucid1  6144  ncdisjeq  6149  tcdi  6165  sbthlem3  6206  addlec  6209  nc0le1  6217  dflec3  6222  nclenc  6223  lenc  6224  tc11  6229  taddc  6230  letc  6232  ce2le  6234  cet  6235  te0c  6238  ce0lenc1  6240  tlenc1c  6241  addcdi  6251  muc0or  6253  nchoicelem8  6297  nchoicelem12  6301  nchoicelem14  6303  frecxp  6315  scancan  6332