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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  syl222anc  1386  vtocldf  3541  f1oprswap  6877  dmdcand  12021  modmul12d  13892  modnegd  13893  modadd12d  13894  exprec  14071  rpexpmord  14135  splval2  14709  dvdsmodexp  16207  eulerthlem2  16717  fermltl  16719  odzdvds  16730  fnpr2o  17505  efgredleme  19613  efgredlemc  19615  blssps  23937  blss  23938  metequiv2  24026  met1stc  24037  met2ndci  24038  metdstri  24374  xlebnum  24488  caubl  24832  divcxp  26202  cxple2a  26214  cxplead  26236  cxplt2d  26241  cxple2d  26242  mulcxpd  26243  ang180  26326  wilthlem2  26580  lgsvalmod  26826  lgsmod  26833  lgsdir2lem4  26838  lgsdirprm  26841  lgsne0  26845  lgseisen  26889  conway  27308  ax5seglem9  28233  fzm1ne1  32038  xrsmulgzz  32217  linds2eq  32542  heiborlem8  36772  cdlemd4  39158  cdleme15a  39231  cdleme17b  39244  cdleme25a  39310  cdleme25c  39312  cdleme25dN  39313  cdleme26ee  39317  tendococl  39729  tendodi1  39741  tendodi2  39742  cdlemi  39777  tendocan  39781  cdlemk5a  39792  cdlemk5  39793  cdlemk10  39800  cdlemk5u  39818  cdlemkfid1N  39878  pellexlem6  41654  acongeq  41804  jm2.25  41820  stoweidlem42  44837  stoweidlem51  44846  ldepspr  47232