Theorem syl32anc 1281

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

Hypotheses

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

Assertion

Ref	Expression
syl32anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl32anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. 2 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. 2 ⊢ (𝜑 → 𝜃)
4		sylXanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		sylXanc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 306	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl32anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl31anc 1276	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

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

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  ioom  10521  modifeq2int  10649  modaddmodup  10650  seq3f1olemqsum  10776  seq3f1o  10780  exple1  10858  leexp2rd  10966  nn0ltexp2  10972  facubnd  11008  permnn  11034  dfabsmax  11779  expcnvre  12066  dvdsadd2b  12403  dvdsmulgcd  12598  sqgcd  12602  bezoutr  12605  cncongr2  12678  pw2dvds  12740  hashgcdlem  12812  modprm0  12829  modprmn0modprm0  12831  2idlcpblrng  14540  tgioo  15281  mpodvdsmulf1o  15717  perfectlem2  15727  lgssq  15772  lgssq2  15773  gausslemma2dlem7  15800  lgsquad2lem1  15813  lgsquad2lem2  15814