Theorem syl221anc 1329

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

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

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

This theorem is referenced by:  syl222anc  1334  vtocldf  3229  f1oprswap  6092  dmdcand  10709  modmul12d  12586  modnegd  12587  modadd12d  12588  exprec  12763  splval2  13359  eulerthlem2  15325  fermltl  15327  odzdvds  15338  efgredleme  17979  efgredlemc  17981  blssps  22039  blss  22040  metequiv2  22125  met1stc  22136  met2ndci  22137  metdstri  22462  xlebnum  22572  caubl  22914  divcxp  24233  cxple2a  24245  cxplead  24267  cxplt2d  24272  cxple2d  24273  mulcxpd  24274  ang180  24344  wilthlem2  24595  lgslem4  24825  lgsvalmod  24841  lgsmod  24848  lgsdir2lem4  24853  lgsdirprm  24856  lgsne0  24860  lgseisen  24904  ax5seglem9  25617  xrsmulgzz  29009  heiborlem8  32787  cdlemd4  34506  cdleme15a  34579  cdleme17b  34592  cdleme25a  34659  cdleme25c  34661  cdleme25dN  34662  cdleme26ee  34666  tendococl  35078  tendodi1  35090  tendodi2  35091  cdlemi  35126  tendocan  35130  cdlemk5a  35141  cdlemk5  35142  cdlemk10  35149  cdlemk5u  35167  cdlemkfid1N  35227  pellexlem6  36416  rpexpmord  36531  acongeq  36568  jm2.25  36584  stoweidlem42  38935  stoweidlem51  38944  ldepspr  42056