Theorem syl221anc 1381

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 1376	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  1386  vtocldf  3572  f1oprswap  6906  dmdcand  12099  modmul12d  13976  modnegd  13977  modadd12d  13978  exprec  14154  rpexpmord  14218  splval2  14805  dvdsmodexp  16310  eulerthlem2  16829  fermltl  16831  odzdvds  16842  fnpr2o  17617  efgredleme  19785  efgredlemc  19787  blssps  24455  blss  24456  metequiv2  24544  met1stc  24555  met2ndci  24556  metdstri  24892  xlebnum  25016  caubl  25361  divcxp  26747  cxple2a  26759  cxplead  26781  cxplt2d  26786  cxple2d  26787  mulcxpd  26788  ang180  26875  wilthlem2  27130  lgsvalmod  27378  lgsmod  27385  lgsdir2lem4  27390  lgsdirprm  27393  lgsne0  27397  lgseisen  27441  conway  27862  ax5seglem9  28970  fzm1ne1  32794  xrsmulgzz  32992  linds2eq  33374  heiborlem8  37778  cdlemd4  40158  cdleme15a  40231  cdleme17b  40244  cdleme25a  40310  cdleme25c  40312  cdleme25dN  40313  cdleme26ee  40317  tendococl  40729  tendodi1  40741  tendodi2  40742  cdlemi  40777  tendocan  40781  cdlemk5a  40792  cdlemk5  40793  cdlemk10  40800  cdlemk5u  40818  cdlemkfid1N  40878  pellexlem6  42790  acongeq  42940  jm2.25  42956  stoweidlem42  45963  stoweidlem51  45972  ldepspr  48202