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  10859  nn0leexp2  10973  expcanlem  10978  expcand  10980  swrds1  11250  ccatswrd  11252  pfxfv  11266  swrdccatin1  11307  pfxccatin12lem3  11314  xrmaxaddlem  11822  mertenslemi1  12098  eftlub  12253  dvdsadd  12399  3dvds  12427  divalgmod  12490  bitsfzolem  12517  bitsfzo  12518  bitsmod  12519  bitsinv1lem  12524  gcdzeq  12595  rplpwr  12600  sqgcd  12602  bezoutr  12605  rpmulgcd2  12669  rpdvds  12673  isprm5  12716  divgcdodd  12717  oddpwdclemxy  12743  divnumden  12770  crth  12798  phimullem  12799  coprimeprodsq2  12833  pythagtriplem19  12857  pclemub  12862  pcpre1  12867  pcidlem  12898  pockthlem  12931  prmunb  12937  kerf1ghm  13863  elrhmunit  14194  rrgnz  14285  znunit  14676  xblss2ps  15131  xblss2  15132  metcnpi3  15244  limcimolemlt  15391  limccnp2cntop  15404  dvmulxxbr  15429  dvcoapbr  15434  ltexp2d  15669  mpodvdsmulf1o  15717  lgsquad2lem2  15814  2lgsoddprmlem1  15837  2sqlem8a  15854  2sqlem8  15855