Theorem syl221anc 1378

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  syl222anc  1383  vtocldf  3540  f1oprswap  6877  dmdcand  12062  modmul12d  13937  modnegd  13938  modadd12d  13939  exprec  14115  rpexpmord  14179  splval2  14758  dvdsmodexp  16257  eulerthlem2  16777  fermltl  16779  odzdvds  16790  fnpr2o  17565  efgredleme  19735  efgredlemc  19737  blssps  24416  blss  24417  metequiv2  24505  met1stc  24516  met2ndci  24517  metdstri  24853  xlebnum  24977  caubl  25322  divcxp  26709  cxple2a  26721  cxplead  26743  cxplt2d  26748  cxple2d  26749  mulcxpd  26750  ang180  26837  wilthlem2  27092  lgsvalmod  27340  lgsmod  27347  lgsdir2lem4  27352  lgsdirprm  27355  lgsne0  27359  lgseisen  27403  conway  27824  ax5seglem9  28866  fzm1ne1  32692  xrsmulgzz  32890  linds2eq  33260  heiborlem8  37530  cdlemd4  39911  cdleme15a  39984  cdleme17b  39997  cdleme25a  40063  cdleme25c  40065  cdleme25dN  40066  cdleme26ee  40070  tendococl  40482  tendodi1  40494  tendodi2  40495  cdlemi  40530  tendocan  40534  cdlemk5a  40545  cdlemk5  40546  cdlemk10  40553  cdlemk5u  40571  cdlemkfid1N  40631  pellexlem6  42526  acongeq  42676  jm2.25  42692  stoweidlem42  45697  stoweidlem51  45706  ldepspr  47890