Theorem syl31anc 1219

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

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
sylXanc.4	⊢ (𝜑 → 𝜏)
syl31anc.5	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl31anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl31anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1161	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		sylXanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl31anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	4, 5, 6	syl2anc 408	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  syl32anc  1224  stoic4b  1409  enq0tr  7235  ltmul12a  8611  lt2msq1  8636  ledivp1  8654  lemul1ad  8690  lemul2ad  8691  lediv2ad  9499  xaddge0  9654  difelfznle  9905  expubnd  10343  expcanlem  10455  expcand  10457  xrmaxaddlem  11022  mertenslemi1  11297  eftlub  11385  dvdsadd  11525  divalgmod  11613  gcdzeq  11699  rplpwr  11704  sqgcd  11706  bezoutr  11709  rpmulgcd2  11765  rpdvds  11769  divgcdodd  11810  oddpwdclemxy  11836  divnumden  11863  crth  11889  phimullem  11890  xblss2ps  12562  xblss2  12563  metcnpi3  12675  limcimolemlt  12791  limccnp2cntop  12804  dvmulxxbr  12824  dvcoapbr  12829