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  7216  enq0tr  7754  ltmul12a  9139  lt2msq1  9164  ledivp1  9182  lemul1ad  9218  lemul2ad  9219  lediv2ad  10058  xaddge0  10217  difelfznle  10476  expubnd  10965  nn0leexp2  11080  expcanlem  11085  expcand  11087  hashmap  11200  swrds1  11368  ccatswrd  11370  pfxfv  11384  swrdccatin1  11425  pfxccatin12lem3  11432  xrmaxaddlem  11953  mertenslemi1  12229  eftlub  12384  dvdsadd  12530  3dvds  12558  divalgmod  12621  bitsfzolem  12648  bitsfzo  12649  bitsmod  12650  bitsinv1lem  12655  gcdzeq  12726  rplpwr  12731  sqgcd  12733  bezoutr  12736  rpmulgcd2  12800  rpdvds  12804  isprm5  12847  divgcdodd  12848  oddpwdclemxy  12874  divnumden  12901  crth  12929  phimullem  12930  coprimeprodsq2  12964  pythagtriplem19  12988  pclemub  12993  pcpre1  12998  pcidlem  13029  pockthlem  13062  prmunb  13068  kerf1ghm  14012  elrhmunit  14344  rrgnz  14437  znunit  14856  xblss2ps  15318  xblss2  15319  metcnpi3  15431  limcimolemlt  15578  limccnp2cntop  15591  dvmulxxbr  15616  dvcoapbr  15621  ltexp2d  15856  pellexlem3  15896  mpodvdsmulf1o  15907  lgsquad2lem2  16004  2lgsoddprmlem1  16027  2sqlem8a  16044  2sqlem8  16045