Theorem syl2an 463

Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.)

Hypotheses

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

Assertion

Ref	Expression
syl2an	|- ((ph /\ ta) -> th)

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		syl2an.2	. 2 |- (ta -> ch)
2		syl2an.1	. . 3 |- (ph -> ps)
3		syl2an.3	. . 3 |- ((ps /\ ch) -> th)
4	2, 3	sylan 457	. 2 |- ((ph /\ ch) -> th)
5	1, 4	sylan2 460	1 |- ((ph /\ ta) -> 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:  syl2anr  464  anim12i  549  ax11indalem  2197  eqeqan12d  2368  sylan9eq  2405  csbcomg  3160  sylan9ss  3286  ssconb  3400  ineqan12d  3460  ifpr  3775  unexg  4102  opkelopkabg  4246  opkelcokg  4262  opkelimagekg  4272  xpkexg  4289  cokexg  4310  ncfinlower  4484  tfindi  4497  tfinlefin  4503  vfinspsslem1  4551  opexg  4588  copsex2g  4610  breqan12d  4655  coexg  4750  opbrop  4842  dmpropg  5069  xpexg  5115  funssres  5145  fnco  5192  fcnvres  5244  fodmrnu  5278  fvun1  5380  fconst2g  5453  isomin  5497  oveqan12d  5542  ovg  5602  txpexg  5785  cupvalg  5813  pprodexg  5838  ovcross  5846  qsexg  5983  mapvalg  6010  pmvalg  6011  mapsn  6027  xpassen  6058  enmap1lem5  6074  enprmaplem3  6079  ncaddccl  6145  ncdisjeq  6149  ovcelem1  6172  cenc  6182  sbthlem1  6204  sbthlem3  6206  lectr  6212  leconnnc  6219  tlecg  6231  nmembers1lem3  6271  nnc3n3p1  6279  nnc3n3p2  6280  nnc3p1n3p2  6281  nchoicelem5  6294  nchoicelem17  6306