Theorem syl311anc 1411

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl311anc.6	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)

Assertion

Ref	Expression
syl311anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl311anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1146	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl311anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)
8	4, 5, 6, 7	syl3anc 1398	1 ⊢ (𝜑 → 𝜁)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl312anc  1418  syl321anc  1419  syl313anc  1421  syl331anc  1422  fprlem1  8322  pythagtrip  17018  nmolb2d  25043  nmoleub  25056  clwwisshclwwslem  30611  numclwwlk1lem2foa  30961  cvlcvr1  40490  4atlem12b  40762  dalawlem10  41031  dalawlem13  41034  dalawlem15  41036  osumcllem11N  41117  lhp2atne  41185  lhp2at0ne  41187  cdlemd  41358  ltrneq3  41359  cdleme7d  41397  cdlemeg49le  41662  cdleme  41711  cdlemg1a  41721  ltrniotavalbN  41735  cdlemg44  41884  cdlemk19  42020  cdlemk27-3  42058  cdlemk33N  42060  cdlemk34  42061  cdlemk49  42102  cdlemk53a  42106  cdlemk19u  42121  cdlemk56w  42124  dia2dimlem4  42218  dih1dimatlem0  42479  itsclc0yqe  49967  itsclinecirc0  49979  itsclinecirc0b  49980  itscnhlinecirc02p  49991  inlinecirc02plem  49992