Theorem syld3an1 1372

Description: A syllogism inference. (Contributed by NM, 7-Jul-2008.)

Hypotheses

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

Assertion

Ref	Expression
syld3an1	|- ( ( ch /\ ps /\ th ) -> ta )

Proof of Theorem syld3an1

Step	Hyp	Ref	Expression
1		syld3an1.1	. . . 4 |- ( ( ch /\ ps /\ th ) -> ph )
2	1	3com13 1270	. . 3 |- ( ( th /\ ps /\ ch ) -> ph )
3		syld3an1.2	. . . 4 |- ( ( ph /\ ps /\ th ) -> ta )
4	3	3com13 1270	. . 3 |- ( ( th /\ ps /\ ph ) -> ta )
5	2, 4	syld3an3 1371	. 2 |- ( ( th /\ ps /\ ch ) -> ta )
6	5	3com13 1270	1 |- ( ( ch /\ ps /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  npncan  10302  nnpcan  10304  ppncan  10323  muldivdir  10720  div2neg  10748  ltmuldiv  10896  opfi1uzind  13283  opfi1uzindOLD  13289  sgrp2nmndlem4  17415  zndvds  19898  subdivcomb1  31611  wsuceq123  31760  atlrelat1  34608  cvlatcvr1  34628  dih11  36554  mullimc  39848  mullimcf  39855  icccncfext  40100  stoweidlem34  40251  stoweidlem49  40266  stoweidlem57  40274  sigarexp  41048  el0ldepsnzr  42256