Theorem syl221anc 1488

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 555	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl221anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 2, 5, 6, 7	syl211anc 1483	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 385  df-3an 1074

This theorem is referenced by:  syl222anc  1493  vtocldf  3396  f1oprswap  6342  dmdcand  11042  modmul12d  12938  modnegd  12939  modadd12d  12940  exprec  13115  splval2  13728  dvdsmodexp  15210  eulerthlem2  15709  fermltl  15711  odzdvds  15722  efgredleme  18376  efgredlemc  18378  blssps  22450  blss  22451  metequiv2  22536  met1stc  22547  met2ndci  22548  metdstri  22875  xlebnum  22985  caubl  23326  divcxp  24653  cxple2a  24665  cxplead  24687  cxplt2d  24692  cxple2d  24693  mulcxpd  24694  ang180  24764  wilthlem2  25015  lgsvalmod  25261  lgsmod  25268  lgsdir2lem4  25273  lgsdirprm  25276  lgsne0  25280  lgseisen  25324  ax5seglem9  26037  xrsmulgzz  30008  conway  32237  etasslt  32247  heiborlem8  33948  cdlemd4  36009  cdleme15a  36082  cdleme17b  36095  cdleme25a  36161  cdleme25c  36163  cdleme25dN  36164  cdleme26ee  36168  tendococl  36580  tendodi1  36592  tendodi2  36593  cdlemi  36628  tendocan  36632  cdlemk5a  36643  cdlemk5  36644  cdlemk10  36651  cdlemk5u  36669  cdlemkfid1N  36729  pellexlem6  37918  rpexpmord  38033  acongeq  38070  jm2.25  38086  stoweidlem42  40780  stoweidlem51  40789  ldepspr  42790