Theorem syl3an2 860

Description: A syllogism inference.

Hypotheses

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

Assertion

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

Proof of Theorem syl3an2

Step	Hyp	Ref	Expression
1		syl3an.1	. . . 4 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 832	. . 3 |- (ph -> (ps -> (ch -> th)))
3		syl3an2.2	. . 3 |- (ta -> ps)
4	2, 3	syl5 21	. 2 |- (ph -> (ta -> (ch -> th)))
5	4	3imp 827	1 |- ((ph /\ ta /\ ch) -> th)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  syl3an2b 863  syl3an2br 866  syl3anl2 874  fvco3 3776  odi 4210  omass 4211  subcant 5412  lesub2t 5661  ltsub2t 5663  ltdiv2t 5887  supxrunb1 6089  peano2uz 6447  expge0t 6591  expordit 6600  absrpclt 6855  absdifltt 6883  absdiflet 6884  fsumshftm 7032  climsqueeze 7140  climsqueeze2 7141  caucvglem2 7158  caucvglem5 7161  iserzgt0 7211  expcnvlem2 7228  cvgratlem2ALT 7248  cvgratlem2 7251  cvgratlem5 7254  erelem3 7321  2basgent 7641  dnsconst 7788  bcthlem1 7999  nvsge0 8291  nmoub3i 8436  nmobndi 8438  ipblnfi 8516  spwpr3OLD 8662  hvsubdistr2t 8917  hvsubcant 8941  his2subt 8958  projlem26 9211  chlubt 9432  homco1t 9727  homulasst 9728  nmopub2tALT 9833  nmfnleub2t 9850  homco2t 9901  cnlnadjlem2 10001  adjmult 10025  irredlem2 10318  atmd2 10327  mdsymlem5 10334  rcfpfil 10597  rcfpfilOLD 10598

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