Theorem sylan 457

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

Hypotheses

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

Assertion

Ref	Expression
sylan	|- ((ph /\ ch) -> th)

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- (ph -> ps)
2		sylan.2	. . 3 |- ((ps /\ ch) -> th)
3	2	expcom 424	. 2 |- (ch -> (ps -> th))
4	1, 3	mpan9 455	1 |- ((ph /\ ch) -> 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:  sylanb  458  sylanbr  459  syl2an  463  sylanl1  631  sylanl2  632  mpanl1  661  mpanl2  662  adantll  694  adantlr  695  ancom1s  780  3adantl1  1111  3adantl2  1112  3adantl3  1113  syl3anl1  1230  syl3anl3  1232  syl3anl  1233  sbcom  2089  eupick  2267  sbcrext  3120  csbiebt  3173  csbnestgf  3185  reuss2  3536  opkthg  4132  iota2  4368  addcexg  4394  lefinlteq  4464  ltlefin  4469  tfinsuc  4499  eventfin  4518  oddtfin  4519  opelopabt  4700  imaexg  4747  ideqg2  4870  imadif  5172  fnbr  5186  feu  5243  fcnvres  5244  f1ss  5263  dffo2  5274  foco  5280  fun11iun  5306  ffoss  5315  fvco3  5385  fvopabg  5392  elpreima  5408  ffvelrn  5416  dffo4  5424  foelrn  5426  fsn2  5435  fvconst2g  5452  funfvima  5460  f1elima  5475  f1ocnvfv1  5477  f1ocnvfv2  5478  f1ofveu  5481  f1ocnvdm  5482  isocnv  5492  isores2  5494  isotr  5496  isoini  5498  f1oiso  5500  f1oiso2  5501  eloprabga  5579  mpteq12  5658  enprmaplem3  6079  ovmuc  6131  mucnc  6132  cenc  6182  leaddc1  6215  addccan2nc  6266  lecadd2  6267  nnc3n3p2  6280  nchoicelem4  6293  nchoicelem5  6294  nchoicelem8  6297