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 ⊢ (𝜑 → 𝜂)

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

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 1011

This theorem is referenced by:  syl32anc  1286  stoic4b  1482  mapfi  7255  enq0tr  7795  ltmul12a  9184  lt2msq1  9209  ledivp1  9227  lemul1ad  9263  lemul2ad  9264  lediv2ad  10103  xaddge0  10263  difelfznle  10525  expubnd  11016  nn0leexp2  11131  expcanlem  11136  expcand  11138  hashmap  11251  swrds1  11423  ccatswrd  11425  pfxfv  11439  swrdccatin1  11480  pfxccatin12lem3  11487  xrmaxaddlem  12009  mertenslemi1  12285  eftlub  12440  dvdsadd  12586  3dvds  12614  divalgmod  12677  bitsfzolem  12704  bitsfzo  12705  bitsmod  12706  bitsinv1lem  12711  gcdzeq  12782  rplpwr  12787  sqgcd  12789  bezoutr  12792  rpmulgcd2  12856  rpdvds  12860  isprm5  12903  divgcdodd  12904  oddpwdclemxy  12930  divnumden  12957  crth  12985  phimullem  12986  coprimeprodsq2  13020  pythagtriplem19  13044  pclemub  13049  pcpre1  13054  pcidlem  13085  pockthlem  13118  prmunb  13124  kerf1ghm  14060  elrhmunit  14467  rrgnz  14560  znunit  14977  xblss2ps  15488  xblss2  15489  metcnpi3  15601  limcimolemlt  15748  limccnp2cntop  15761  dvmulxxbr  15786  dvcoapbr  15791  ltexp2d  16027  pellexlem3  16076  mpodvdsmulf1o  16087  lgsquad2lem2  16184  2lgsoddprmlem1  16207  2sqlem8a  16224  2sqlem8  16225