Theorem syl3an2 859

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 831	. . 3 |- (ph -> (ps -> (ch -> th)))
3		syl3an2.2	. . 3 |- (ta -> ps)
4	2, 3	syl5 21	. 2 |- (ph -> (ta -> (ch -> th)))
5	4	3imp 826	1 |- ((ph /\ ta /\ ch) -> th)

Syntax hints:   -> wi 3   /\ w3a 774

This theorem is referenced by:  syl3an2b 862  syl3an2br 865  syl3anl2 872  fvco3 3767  odi 4200  omass 4201  subcant 5392  lesub2t 5642  ltsub2t 5644  ltdiv2t 5843  ltdiv23t 5848  lediv23t 5849  supxrunb1 6044  peano2uz 6387  expge0t 6530  expordit 6539  absrpclt 6798  absdifltt 6829  absdiflet 6830  fsumshftm 6978  climsqueeze 7084  climsqueeze2 7085  caucvglem2 7102  caucvglem5 7105  iserzgt0 7154  expcnvlem2 7171  cvgratlem2ALT 7191  cvgratlem2 7194  cvgratlem5 7197  erelem3 7271  2basgent 7591  dnsconst 7738  bcthlem1 7949  nvsge0 8243  nmoub3i 8381  nmobndi 8383  ipblnfi 8460  hvsubdistr2t 8856  hvsubcant 8880  his2subt 8897  projlem26 9150  chlubt 9370  homco1t 9667  homulasst 9668  nmopub2tALT 9773  nmfnleub2t 9789  homco2t 9840  cnlnadjlem2 9939  adjmult 9963  irredlem2 10255  atmd2 10264  mdsymlem5 10271

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 776

Copyright terms: Public domain