Theorem syl31anc 1252

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

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

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 982

This theorem is referenced by:  syl32anc  1257  stoic4b  1444  enq0tr  7494  ltmul12a  8879  lt2msq1  8904  ledivp1  8922  lemul1ad  8958  lemul2ad  8959  lediv2ad  9785  xaddge0  9944  difelfznle  10201  expubnd  10667  nn0leexp2  10781  expcanlem  10786  expcand  10788  xrmaxaddlem  11403  mertenslemi1  11678  eftlub  11833  dvdsadd  11979  divalgmod  12068  gcdzeq  12159  rplpwr  12164  sqgcd  12166  bezoutr  12169  rpmulgcd2  12233  rpdvds  12237  isprm5  12280  divgcdodd  12281  oddpwdclemxy  12307  divnumden  12334  crth  12362  phimullem  12363  coprimeprodsq2  12396  pythagtriplem19  12420  pclemub  12425  pcpre1  12430  pcidlem  12461  pockthlem  12494  prmunb  12500  kerf1ghm  13344  elrhmunit  13673  rrgnz  13764  znunit  14147  xblss2ps  14572  xblss2  14573  metcnpi3  14685  limcimolemlt  14818  limccnp2cntop  14831  dvmulxxbr  14851  dvcoapbr  14856  2lgsoddprmlem1  15193  2sqlem8a  15209  2sqlem8  15210