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  7659  ltmul12a  9045  lt2msq1  9070  ledivp1  9088  lemul1ad  9124  lemul2ad  9125  lediv2ad  9959  xaddge0  10118  difelfznle  10375  expubnd  10864  nn0leexp2  10978  expcanlem  10983  expcand  10985  swrds1  11258  ccatswrd  11260  pfxfv  11274  swrdccatin1  11315  pfxccatin12lem3  11322  xrmaxaddlem  11843  mertenslemi1  12119  eftlub  12274  dvdsadd  12420  3dvds  12448  divalgmod  12511  bitsfzolem  12538  bitsfzo  12539  bitsmod  12540  bitsinv1lem  12545  gcdzeq  12616  rplpwr  12621  sqgcd  12623  bezoutr  12626  rpmulgcd2  12690  rpdvds  12694  isprm5  12737  divgcdodd  12738  oddpwdclemxy  12764  divnumden  12791  crth  12819  phimullem  12820  coprimeprodsq2  12854  pythagtriplem19  12878  pclemub  12883  pcpre1  12888  pcidlem  12919  pockthlem  12952  prmunb  12958  kerf1ghm  13884  elrhmunit  14215  rrgnz  14306  znunit  14697  xblss2ps  15157  xblss2  15158  metcnpi3  15270  limcimolemlt  15417  limccnp2cntop  15430  dvmulxxbr  15455  dvcoapbr  15460  ltexp2d  15695  mpodvdsmulf1o  15743  lgsquad2lem2  15840  2lgsoddprmlem1  15863  2sqlem8a  15880  2sqlem8  15881