Theorem syl31anc 1274

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

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

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 1004

This theorem is referenced by:  syl32anc  1279  stoic4b  1475  enq0tr  7637  ltmul12a  9023  lt2msq1  9048  ledivp1  9066  lemul1ad  9102  lemul2ad  9103  lediv2ad  9932  xaddge0  10091  difelfznle  10348  expubnd  10835  nn0leexp2  10949  expcanlem  10954  expcand  10956  swrds1  11221  ccatswrd  11223  pfxfv  11237  swrdccatin1  11278  pfxccatin12lem3  11285  xrmaxaddlem  11792  mertenslemi1  12067  eftlub  12222  dvdsadd  12368  3dvds  12396  divalgmod  12459  bitsfzolem  12486  bitsfzo  12487  bitsmod  12488  bitsinv1lem  12493  gcdzeq  12564  rplpwr  12569  sqgcd  12571  bezoutr  12574  rpmulgcd2  12638  rpdvds  12642  isprm5  12685  divgcdodd  12686  oddpwdclemxy  12712  divnumden  12739  crth  12767  phimullem  12768  coprimeprodsq2  12802  pythagtriplem19  12826  pclemub  12831  pcpre1  12836  pcidlem  12867  pockthlem  12900  prmunb  12906  kerf1ghm  13832  elrhmunit  14162  rrgnz  14253  znunit  14644  xblss2ps  15099  xblss2  15100  metcnpi3  15212  limcimolemlt  15359  limccnp2cntop  15372  dvmulxxbr  15397  dvcoapbr  15402  ltexp2d  15637  mpodvdsmulf1o  15685  lgsquad2lem2  15782  2lgsoddprmlem1  15805  2sqlem8a  15822  2sqlem8  15823