Theorem syl31anc 1277

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

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

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 1007

This theorem is referenced by:  syl32anc  1282  stoic4b  1478  mapfi  7227  enq0tr  7765  ltmul12a  9154  lt2msq1  9179  ledivp1  9197  lemul1ad  9233  lemul2ad  9234  lediv2ad  10073  xaddge0  10233  difelfznle  10494  expubnd  10985  nn0leexp2  11100  expcanlem  11105  expcand  11107  hashmap  11220  swrds1  11388  ccatswrd  11390  pfxfv  11404  swrdccatin1  11445  pfxccatin12lem3  11452  xrmaxaddlem  11973  mertenslemi1  12249  eftlub  12404  dvdsadd  12550  3dvds  12578  divalgmod  12641  bitsfzolem  12668  bitsfzo  12669  bitsmod  12670  bitsinv1lem  12675  gcdzeq  12746  rplpwr  12751  sqgcd  12753  bezoutr  12756  rpmulgcd2  12820  rpdvds  12824  isprm5  12867  divgcdodd  12868  oddpwdclemxy  12894  divnumden  12921  crth  12949  phimullem  12950  coprimeprodsq2  12984  pythagtriplem19  13008  pclemub  13013  pcpre1  13018  pcidlem  13049  pockthlem  13082  prmunb  13088  kerf1ghm  14030  elrhmunit  14425  rrgnz  14518  znunit  14936  xblss2ps  15398  xblss2  15399  metcnpi3  15511  limcimolemlt  15658  limccnp2cntop  15671  dvmulxxbr  15696  dvcoapbr  15701  ltexp2d  15936  pellexlem3  15976  mpodvdsmulf1o  15987  lgsquad2lem2  16084  2lgsoddprmlem1  16107  2sqlem8a  16124  2sqlem8  16125