Theorem syl31anc 1281

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl32anc  1286  stoic4b  1482  mapfi  7261  enq0tr  7801  ltmul12a  9191  lt2msq1  9216  ledivp1  9234  lemul1ad  9270  lemul2ad  9271  lediv2ad  10122  xaddge0  10282  difelfznle  10544  expubnd  11035  nn0leexp2  11150  expcanlem  11155  expcand  11157  hashmap  11270  swrds1  11442  ccatswrd  11444  pfxfv  11458  swrdccatin1  11499  pfxccatin12lem3  11506  xrmaxaddlem  12028  mertenslemi1  12304  eftlub  12459  dvdsadd  12605  3dvds  12633  divalgmod  12696  bitsfzolem  12723  bitsfzo  12724  bitsmod  12725  bitsinv1lem  12730  gcdzeq  12801  rplpwr  12806  sqgcd  12808  bezoutr  12811  rpmulgcd2  12875  rpdvds  12879  isprm5  12922  divgcdodd  12923  oddpwdclemxy  12949  divnumden  12976  crth  13004  phimullem  13005  coprimeprodsq2  13039  pythagtriplem19  13063  pclemub  13068  pcpre1  13073  pcidlem  13104  pockthlem  13137  prmunb  13143  kerf1ghm  14079  elrhmunit  14486  rrgnz  14579  znunit  14996  xblss2ps  15507  xblss2  15508  metcnpi3  15620  limcimolemlt  15767  limccnp2cntop  15780  dvmulxxbr  15805  dvcoapbr  15810  ltexp2d  16050  pellexlem3  16099  mpodvdsmulf1o  16110  lgsquad2lem2  16213  2lgsoddprmlem1  16236  2sqlem8a  16253  2sqlem8  16254