Theorem syl221anc 1380

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 1375	1 ⊢ (𝜑 → 𝜁)

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

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 1088

This theorem is referenced by:  syl222anc  1385  vtocldf  3560  f1oprswap  6893  dmdcand  12070  modmul12d  13963  modnegd  13964  modadd12d  13965  exprec  14141  rpexpmord  14205  splval2  14792  dvdsmodexp  16295  eulerthlem2  16816  fermltl  16818  odzdvds  16829  fnpr2o  17604  efgredleme  19776  efgredlemc  19778  blssps  24450  blss  24451  metequiv2  24539  met1stc  24550  met2ndci  24551  metdstri  24887  xlebnum  25011  caubl  25356  divcxp  26744  cxple2a  26756  cxplead  26778  cxplt2d  26783  cxple2d  26784  mulcxpd  26785  ang180  26872  wilthlem2  27127  lgsvalmod  27375  lgsmod  27382  lgsdir2lem4  27387  lgsdirprm  27390  lgsne0  27394  lgseisen  27438  conway  27859  ax5seglem9  28967  fzm1ne1  32797  xrsmulgzz  32994  linds2eq  33389  heiborlem8  37805  cdlemd4  40184  cdleme15a  40257  cdleme17b  40270  cdleme25a  40336  cdleme25c  40338  cdleme25dN  40339  cdleme26ee  40343  tendococl  40755  tendodi1  40767  tendodi2  40768  cdlemi  40803  tendocan  40807  cdlemk5a  40818  cdlemk5  40819  cdlemk10  40826  cdlemk5u  40844  cdlemkfid1N  40904  pellexlem6  42822  acongeq  42972  jm2.25  42988  stoweidlem42  45998  stoweidlem51  46007  ldepspr  48319