Theorem syld3an3 870

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		syl3an.1	. 2 |- ((ph /\ ps /\ ch) -> th)
2		3simp1 788	. 2 |- ((ph /\ ps /\ ta) -> ph)
3		3simp2 789	. 2 |- ((ph /\ ps /\ ta) -> ps)
4		syld3an3.2	. 2 |- ((ph /\ ps /\ ta) -> ch)
5	1, 2, 3, 4	syl3anc 858	1 |- ((ph /\ ps /\ ta) -> th)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  syld3an1 871  syld3an2 872  brelrng 3343  omwordri 4203  oewordri 4219  lediv1t 5851  lt2mul2divt 5872  lemuldivt 5874  supxrbnd 6091  znnenlem 7501  opnneiss 7732  metcni2 7895  lmfexlem3 7958  grpdivinv 8083  grpinvdiv 8084  grpdivf 8085  vcnegsubdi2 8194  vcsub4 8195  nvsubadd 8275  nvaddsub4 8281  nvnncan 8283  nvpi 8294  nvmtri 8299  nvabs 8301  nvelbl2 8326  nvcni 8329  nvcni2 8330  nvcni3 8331  4ipval2 8358  ipval3 8359  isblo2 8443  blof 8445  nmblore 8446  nmlnoubi 8456  nmlnogt0 8457  sincosq1lem 8703  shsubclt 9089  unopadjt 9843  atexcht 10308  atcvatlem 10312  ghomf1olem 10396  dmse2 10624  2wsms 10630

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 147  df-an 225  df-3an 777

Copyright terms: Public domain