Theorem syl31anc 1251

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

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

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 981

This theorem is referenced by:  syl32anc  1256  stoic4b  1443  enq0tr  7447  ltmul12a  8831  lt2msq1  8856  ledivp1  8874  lemul1ad  8910  lemul2ad  8911  lediv2ad  9733  xaddge0  9892  difelfznle  10149  expubnd  10591  nn0leexp2  10704  expcanlem  10709  expcand  10711  xrmaxaddlem  11282  mertenslemi1  11557  eftlub  11712  dvdsadd  11857  divalgmod  11946  gcdzeq  12037  rplpwr  12042  sqgcd  12044  bezoutr  12047  rpmulgcd2  12109  rpdvds  12113  isprm5  12156  divgcdodd  12157  oddpwdclemxy  12183  divnumden  12210  crth  12238  phimullem  12239  coprimeprodsq2  12272  pythagtriplem19  12296  pclemub  12301  pcpre1  12306  pcidlem  12336  pockthlem  12368  prmunb  12374  kerf1ghm  13168  xblss2ps  14257  xblss2  14258  metcnpi3  14370  limcimolemlt  14486  limccnp2cntop  14499  dvmulxxbr  14519  dvcoapbr  14524  2lgsoddprmlem1  14806  2sqlem8a  14822  2sqlem8  14823