Theorem syl31anc 1276

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

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

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 1006

This theorem is referenced by:  syl32anc  1281  stoic4b  1477  enq0tr  7654  ltmul12a  9040  lt2msq1  9065  ledivp1  9083  lemul1ad  9119  lemul2ad  9120  lediv2ad  9954  xaddge0  10113  difelfznle  10370  expubnd  10858  nn0leexp2  10972  expcanlem  10977  expcand  10979  swrds1  11249  ccatswrd  11251  pfxfv  11265  swrdccatin1  11306  pfxccatin12lem3  11313  xrmaxaddlem  11821  mertenslemi1  12097  eftlub  12252  dvdsadd  12398  3dvds  12426  divalgmod  12489  bitsfzolem  12516  bitsfzo  12517  bitsmod  12518  bitsinv1lem  12523  gcdzeq  12594  rplpwr  12599  sqgcd  12601  bezoutr  12604  rpmulgcd2  12668  rpdvds  12672  isprm5  12715  divgcdodd  12716  oddpwdclemxy  12742  divnumden  12769  crth  12797  phimullem  12798  coprimeprodsq2  12832  pythagtriplem19  12856  pclemub  12861  pcpre1  12866  pcidlem  12897  pockthlem  12930  prmunb  12936  kerf1ghm  13862  elrhmunit  14193  rrgnz  14284  znunit  14675  xblss2ps  15130  xblss2  15131  metcnpi3  15243  limcimolemlt  15390  limccnp2cntop  15403  dvmulxxbr  15428  dvcoapbr  15433  ltexp2d  15668  mpodvdsmulf1o  15716  lgsquad2lem2  15813  2lgsoddprmlem1  15836  2sqlem8a  15853  2sqlem8  15854