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  7629  ltmul12a  9015  lt2msq1  9040  ledivp1  9058  lemul1ad  9094  lemul2ad  9095  lediv2ad  9923  xaddge0  10082  difelfznle  10339  expubnd  10826  nn0leexp2  10940  expcanlem  10945  expcand  10947  swrds1  11208  ccatswrd  11210  pfxfv  11224  swrdccatin1  11265  pfxccatin12lem3  11272  xrmaxaddlem  11779  mertenslemi1  12054  eftlub  12209  dvdsadd  12355  3dvds  12383  divalgmod  12446  bitsfzolem  12473  bitsfzo  12474  bitsmod  12475  bitsinv1lem  12480  gcdzeq  12551  rplpwr  12556  sqgcd  12558  bezoutr  12561  rpmulgcd2  12625  rpdvds  12629  isprm5  12672  divgcdodd  12673  oddpwdclemxy  12699  divnumden  12726  crth  12754  phimullem  12755  coprimeprodsq2  12789  pythagtriplem19  12813  pclemub  12818  pcpre1  12823  pcidlem  12854  pockthlem  12887  prmunb  12893  kerf1ghm  13819  elrhmunit  14149  rrgnz  14240  znunit  14631  xblss2ps  15086  xblss2  15087  metcnpi3  15199  limcimolemlt  15346  limccnp2cntop  15359  dvmulxxbr  15384  dvcoapbr  15389  ltexp2d  15624  mpodvdsmulf1o  15672  lgsquad2lem2  15769  2lgsoddprmlem1  15792  2sqlem8a  15809  2sqlem8  15810