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  7213  enq0tr  7745  ltmul12a  9130  lt2msq1  9155  ledivp1  9173  lemul1ad  9209  lemul2ad  9210  lediv2ad  10048  xaddge0  10207  difelfznle  10465  expubnd  10954  nn0leexp2  11068  expcanlem  11073  expcand  11075  swrds1  11353  ccatswrd  11355  pfxfv  11369  swrdccatin1  11410  pfxccatin12lem3  11417  xrmaxaddlem  11938  mertenslemi1  12214  eftlub  12369  dvdsadd  12515  3dvds  12543  divalgmod  12606  bitsfzolem  12633  bitsfzo  12634  bitsmod  12635  bitsinv1lem  12640  gcdzeq  12711  rplpwr  12716  sqgcd  12718  bezoutr  12721  rpmulgcd2  12785  rpdvds  12789  isprm5  12832  divgcdodd  12833  oddpwdclemxy  12859  divnumden  12886  crth  12914  phimullem  12915  coprimeprodsq2  12949  pythagtriplem19  12973  pclemub  12978  pcpre1  12983  pcidlem  13014  pockthlem  13047  prmunb  13053  kerf1ghm  13980  elrhmunit  14311  rrgnz  14403  znunit  14794  xblss2ps  15256  xblss2  15257  metcnpi3  15369  limcimolemlt  15516  limccnp2cntop  15529  dvmulxxbr  15554  dvcoapbr  15559  ltexp2d  15794  pellexlem3  15834  mpodvdsmulf1o  15845  lgsquad2lem2  15942  2lgsoddprmlem1  15965  2sqlem8a  15982  2sqlem8  15983