Theorem sylan2 460

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
sylan2.1	|- (ph -> ch)
sylan2.2	|- ((ps /\ ch) -> th)

Assertion

Ref	Expression
sylan2	|- ((ps /\ ph) -> th)

Proof of Theorem sylan2

Step	Hyp	Ref	Expression
1		sylan2.1	. . 3 |- (ph -> ch)
2	1	adantl 452	. 2 |- ((ps /\ ph) -> ch)
3		sylan2.2	. 2 |- ((ps /\ ch) -> th)
4	2, 3	syldan 456	1 |- ((ps /\ ph) -> th)

Syntax hints:   -> wi 4   /\ wa 358

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  df-an 360

This theorem is referenced by:  sylan2b  461  sylan2br  462  syl2an  463  sylanr1  633  sylanr2  634  mpanr2  665  adantrl  696  adantrr  697  ancom2s  777  3adantr1  1114  3adantr2  1115  3adantr3  1116  syl3anr1  1234  syl3anr3  1236  ax11indalem  2197  ax11inda2ALT  2198  elabgt  2982  sbciegft  3076  csbtt  3148  csbnestgf  3184  difexg  4102  imakexg  4299  dfpw12  4301  pw1eqadj  4332  elsuci  4414  nnsucelr  4428  ltfintr  4459  ltfintri  4466  ncfinlower  4483  tfinpw1  4494  ncfintfin  4495  eventfin  4517  oddtfin  4518  sfindbl  4530  vfinspnn  4541  phi11lem1  4595  copsex2t  4608  resexg  5116  funimass2  5170  dff1o2  5291  resdif  5306  funbrfv  5356  dfimafn  5366  funimass4  5368  eqfnfv2  5393  fvimacnvi  5402  ffvresb  5431  funfvima3  5461  funiunfv  5467  f1elima  5474  isomin  5496  mpt2eq12  5662  fvmptss  5705  ecelqsg  5979  peano4nc  6150  eqtc  6161  dflec3  6221  letc  6231  nclenn  6249  ncslesuc  6267  nmembers1lem3  6270  nchoicelem3  6291  nchoicelem9  6297  nchoicelem17  6305