Theorem syld3an3 1142

Description: A syllogism inference.

Hypotheses

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

Assertion

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

Proof of Theorem syld3an3

Step	Hyp	Ref	Expression
1		simp1 876	. 2 |- ((ph /\ ps /\ ta) -> ph)
2		simp2 877	. 2 |- ((ph /\ ps /\ ta) -> ps)
3		syld3an3.2	. 2 |- ((ph /\ ps /\ ta) -> ch)
4		syl3an.1	. 2 |- ((ph /\ ps /\ ch) -> th)
5	1, 2, 3, 4	syl111anc 1100	1 |- ((ph /\ ps /\ ta) -> th)

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  syld3an1 1143  syld3an2 1144  brelrng 4190  resin 4660  omwordri 5251  oewordri 5267  nnncan1 6632  lediv1 7033  lt2mul2divOLD 7055  lemuldiv 7058  supxrbnd 7300  geoisum1c 8507  znnenlem 8770  opnneiss 9008  metcni2 9173  lmfexlem3 9236  grpdivinv 9368  grpinvdiv 9369  grpdivf 9370  gacan 9460  vcnegsubdi2 9526  vcsub4 9527  nvsubadd 9607  nvaddsub4 9613  nvnncan 9615  nvpi 9626  nvmtri 9631  nvabs 9633  nvelbl2 9658  nvcni 9661  nvcni2 9662  nvcni3 9663  4ipval2 9697  ipval3 9698  isblo2 9783  blof 9785  nmblore 9786  nmlnoubi 9796  nmlnogt0 9797  sincosq1lem 10052  shsubcl 10722  unopadj 11480  atexch 11953  atcvatlem 11957  ghomf1olem 13637  grpdivzer 14740  multinvb 14772  mult2inv 14773  clsint 14860  dmse2 15002  2wsms 15008  flimfneicn 15037  fnctartar3 15286  latmle1 16871  latnle 16880  latabs1 16882  latabs2 16883  opcon2b 16924  opltcon2b 16933  oldmm3 16948  oldmm4 16949  oldmj3 16952  oldmj4 16953  cmt2 16971  cmt4 16973  cvr1 17054  atlene 17071  pmapojoin 17376

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain