Theorem syl221anc 1487

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 383  df-3an 1073

This theorem is referenced by:  syl222anc  1492  vtocldf  3408  f1oprswap  6322  dmdcand  11033  modmul12d  12933  modnegd  12934  modadd12d  12935  exprec  13109  splval2  13718  dvdsmodexp  15198  eulerthlem2  15695  fermltl  15697  odzdvds  15708  efgredleme  18364  efgredlemc  18366  blssps  22450  blss  22451  metequiv2  22536  met1stc  22547  met2ndci  22548  metdstri  22875  xlebnum  22985  caubl  23326  divcxp  24655  cxple2a  24667  cxplead  24689  cxplt2d  24694  cxple2d  24695  mulcxpd  24696  ang180  24766  wilthlem2  25017  lgsvalmod  25263  lgsmod  25270  lgsdir2lem4  25275  lgsdirprm  25278  lgsne0  25282  lgseisen  25326  ax5seglem9  26039  xrsmulgzz  30019  conway  32248  etasslt  32258  heiborlem8  33950  cdlemd4  36011  cdleme15a  36084  cdleme17b  36097  cdleme25a  36163  cdleme25c  36165  cdleme25dN  36166  cdleme26ee  36170  tendococl  36582  tendodi1  36594  tendodi2  36595  cdlemi  36630  tendocan  36634  cdlemk5a  36645  cdlemk5  36646  cdlemk10  36653  cdlemk5u  36671  cdlemkfid1N  36731  pellexlem6  37925  rpexpmord  38040  acongeq  38077  jm2.25  38093  stoweidlem42  40777  stoweidlem51  40786  ldepspr  42791