Theorem syl31anc 1252

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

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

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 982

This theorem is referenced by:  syl32anc  1257  stoic4b  1444  enq0tr  7520  ltmul12a  8906  lt2msq1  8931  ledivp1  8949  lemul1ad  8985  lemul2ad  8986  lediv2ad  9813  xaddge0  9972  difelfznle  10229  expubnd  10707  nn0leexp2  10821  expcanlem  10826  expcand  10828  xrmaxaddlem  11444  mertenslemi1  11719  eftlub  11874  dvdsadd  12020  3dvds  12048  divalgmod  12111  bitsfzolem  12138  bitsfzo  12139  bitsmod  12140  bitsinv1lem  12145  gcdzeq  12216  rplpwr  12221  sqgcd  12223  bezoutr  12226  rpmulgcd2  12290  rpdvds  12294  isprm5  12337  divgcdodd  12338  oddpwdclemxy  12364  divnumden  12391  crth  12419  phimullem  12420  coprimeprodsq2  12454  pythagtriplem19  12478  pclemub  12483  pcpre1  12488  pcidlem  12519  pockthlem  12552  prmunb  12558  kerf1ghm  13482  elrhmunit  13811  rrgnz  13902  znunit  14293  xblss2ps  14748  xblss2  14749  metcnpi3  14861  limcimolemlt  15008  limccnp2cntop  15021  dvmulxxbr  15046  dvcoapbr  15051  ltexp2d  15286  mpodvdsmulf1o  15334  lgsquad2lem2  15431  2lgsoddprmlem1  15454  2sqlem8a  15471  2sqlem8  15472