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  2983  sbciegft  3077  csbtt  3149  csbnestgf  3185  difexg  4103  imakexg  4300  dfpw12  4302  pw1eqadj  4333  elsuci  4415  nnsucelr  4429  ltfintr  4460  ltfintri  4467  ncfinlower  4484  tfinpw1  4495  ncfintfin  4496  eventfin  4518  oddtfin  4519  sfindbl  4531  vfinspnn  4542  phi11lem1  4596  copsex2t  4609  resexg  5117  funimass2  5171  dff1o2  5292  resdif  5307  funbrfv  5357  dfimafn  5367  funimass4  5369  eqfnfv2  5394  fvimacnvi  5403  ffvresb  5432  funfvima3  5462  funiunfv  5468  f1elima  5475  isomin  5497  mpt2eq12  5663  fvmptss  5706  ecelqsg  5980  peano4nc  6151  eqtc  6162  dflec3  6222  letc  6232  nclenn  6250  ncslesuc  6268  nmembers1lem3  6271  nchoicelem3  6292  nchoicelem9  6298  nchoicelem17  6306