Theorem syl221anc 1384

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

Hypotheses

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

Assertion

Ref	Expression
syl221anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl221anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	3, 4	jca 511	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl221anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 2, 5, 6, 7	syl211anc 1379	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl222anc  1389  vtocldf  3505  f1oprswap  6825  dmdcand  11960  modmul12d  13887  modnegd  13888  modadd12d  13889  exprec  14065  rpexpmord  14130  splval2  14719  dvdsmodexp  16229  eulerthlem2  16752  fermltl  16754  odzdvds  16766  fnpr2o  17521  efgredleme  19718  efgredlemc  19720  blssps  24389  blss  24390  metequiv2  24475  met1stc  24486  met2ndci  24487  metdstri  24817  xlebnum  24932  caubl  25275  divcxp  26651  cxple2a  26663  cxplead  26685  cxplt2d  26690  cxple2d  26691  mulcxpd  26692  ang180  26778  wilthlem2  27032  lgsvalmod  27279  lgsmod  27286  lgsdir2lem4  27291  lgsdirprm  27294  lgsne0  27298  lgseisen  27342  conway  27771  ax5seglem9  29006  fzm1ne1  32861  xrsmulgzz  33069  linds2eq  33441  heiborlem8  38139  cdlemd4  40647  cdleme15a  40720  cdleme17b  40733  cdleme25a  40799  cdleme25c  40801  cdleme25dN  40802  cdleme26ee  40806  tendococl  41218  tendodi1  41230  tendodi2  41231  cdlemi  41266  tendocan  41270  cdlemk5a  41281  cdlemk5  41282  cdlemk10  41289  cdlemk5u  41307  cdlemkfid1N  41367  pellexlem6  43262  acongeq  43411  jm2.25  43427  stoweidlem42  46470  stoweidlem51  46479  ldepspr  48949