Theorem syl3anc 629

Description: A syllogism inference combined with contraction.

Hypotheses

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

Assertion

Ref	Expression
syl3anc	|- (ta -> th)

Proof of Theorem syl3anc

Step	Hyp	Ref	Expression
1		syl3anc.2	. . 3 |- (ta -> ph)
2		syl3anc.3	. . 3 |- (ta -> ps)
3		syl3anc.4	. . 3 |- (ta -> ch)
4	1, 2, 3	3jca 604	. 2 |- (ta -> (ph /\ ps /\ ch))
5		syl3anc.1	. 2 |- ((ph /\ ps /\ ch) -> th)
6	4, 5	syl 12	1 |- (ta -> th)

Syntax hints:   -> wi 2   /\ w3a 581

This theorem is referenced by:  oaass 3163  halfpq 3876  divadddivt 4264  divdivdivt 4265  ltsubpost 4364  nnleltp1t 4448  znnsubt 4595  uzind 4603  expaddt 4698  hvsubaddeqt 5019  hi2eqt 5059  pjopt 5264  pjpot 5265  shlej1t 5356  chabs1t 5432  spansncol 5473  pjot 5561  hods 5606  hosass 5607  pjclem4 5653  pj3s 5659  stadd 5687  stadd3 5689  strlem1 5691  golem1 5704  mdbr2 5728  dmdbr2 5733  atexch 5769  atcvatlem 5770  atcvat3 5774

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org