Theorem syl31anc 1187

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 1129	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		sylXanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl31anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	4, 5, 6	syl2anc 406	1 ⊢ (𝜑 → 𝜂)

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

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

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

This theorem is referenced by:  syl32anc  1192  stoic4b  1377  enq0tr  7143  ltmul12a  8476  lt2msq1  8501  ledivp1  8519  lemul1ad  8555  lemul2ad  8556  lediv2ad  9353  xaddge0  9502  difelfznle  9753  expubnd  10191  expcanlem  10303  expcand  10305  xrmaxaddlem  10868  mertenslemi1  11143  eftlub  11194  dvdsadd  11331  divalgmod  11419  gcdzeq  11503  rplpwr  11508  sqgcd  11510  bezoutr  11513  rpmulgcd2  11569  rpdvds  11573  divgcdodd  11614  oddpwdclemxy  11639  divnumden  11666  crth  11692  phimullem  11693  xblss2ps  12332  xblss2  12333  metcnpi3  12441  limcimolemlt  12513