Theorem syl32anc 1260

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 1255	1 ⊢ (𝜑 → 𝜁)

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

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 985

This theorem is referenced by:  ioom  10447  modifeq2int  10575  modaddmodup  10576  seq3f1olemqsum  10702  seq3f1o  10706  exple1  10784  leexp2rd  10892  nn0ltexp2  10898  facubnd  10934  permnn  10960  dfabsmax  11694  expcnvre  11980  dvdsadd2b  12317  dvdsmulgcd  12512  sqgcd  12516  bezoutr  12519  cncongr2  12592  pw2dvds  12654  hashgcdlem  12726  modprm0  12743  modprmn0modprm0  12745  2idlcpblrng  14452  tgioo  15193  mpodvdsmulf1o  15629  perfectlem2  15639  lgssq  15684  lgssq2  15685  gausslemma2dlem7  15712  lgsquad2lem1  15725  lgsquad2lem2  15726