Theorem syl221anc 1337

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl221anc.6	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)

Assertion

Ref	Expression
syl221anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl221anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	3, 4	jca 554	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl221anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 2, 5, 6, 7	syl211anc 1332	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl222anc  1342  vtocldf  3256  f1oprswap  6180  dmdcand  10830  modmul12d  12724  modnegd  12725  modadd12d  12726  exprec  12901  splval2  13508  eulerthlem2  15487  fermltl  15489  odzdvds  15500  efgredleme  18156  efgredlemc  18158  blssps  22229  blss  22230  metequiv2  22315  met1stc  22326  met2ndci  22327  metdstri  22654  xlebnum  22764  caubl  23106  divcxp  24433  cxple2a  24445  cxplead  24467  cxplt2d  24472  cxple2d  24473  mulcxpd  24474  ang180  24544  wilthlem2  24795  lgslem4  25025  lgsvalmod  25041  lgsmod  25048  lgsdir2lem4  25053  lgsdirprm  25056  lgsne0  25060  lgseisen  25104  ax5seglem9  25817  xrsmulgzz  29678  conway  31910  etasslt  31920  heiborlem8  33617  cdlemd4  35488  cdleme15a  35561  cdleme17b  35574  cdleme25a  35641  cdleme25c  35643  cdleme25dN  35644  cdleme26ee  35648  tendococl  36060  tendodi1  36072  tendodi2  36073  cdlemi  36108  tendocan  36112  cdlemk5a  36123  cdlemk5  36124  cdlemk10  36131  cdlemk5u  36149  cdlemkfid1N  36209  pellexlem6  37398  rpexpmord  37513  acongeq  37550  jm2.25  37566  stoweidlem42  40259  stoweidlem51  40268  ldepspr  42262