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  7266  enq0tr  7808  ltmul12a  9199  lt2msq1  9224  ledivp1  9242  lemul1ad  9278  lemul2ad  9279  lediv2ad  10138  xaddge0  10298  difelfznle  10560  expubnd  11055  nn0leexp2  11171  expcanlem  11176  expcand  11178  hashmap  11291  swrds1  11463  ccatswrd  11465  pfxfv  11479  swrdccatin1  11520  pfxccatin12lem3  11527  xrmaxaddlem  12052  mertenslemi1  12328  eftlub  12483  dvdsadd  12629  3dvds  12657  divalgmod  12720  bitsfzolem  12747  bitsfzo  12748  bitsmod  12749  bitsinv1lem  12754  gcdzeq  12825  rplpwr  12830  sqgcd  12832  bezoutr  12835  rpmulgcd2  12899  rpdvds  12903  isprm5  12947  divgcdodd  12948  nnmaxpwlemxy  12974  divnumden  13002  crth  13032  phimullem  13033  coprimeprodsq2  13067  pythagtriplem19  13091  pclemub  13096  pcpre1  13101  pcidlem  13132  pockthlem  13165  prmunb  13171  kerf1ghm  14137  elrhmunit  14594  rrgnz  14687  znunit  15104  xblss2ps  15642  xblss2  15643  metcnpi3  15755  limcimolemlt  15902  limccnp2cntop  15915  dvmulxxbr  15940  dvcoapbr  15945  ltexp2d  16190  pellexlem3  16243  mpodvdsmulf1o  16296  bposlem1  16323  lgsquad2lem2  16418  2lgsoddprmlem1  16441  2sqlem8a  16458  2sqlem8  16459