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  3511  f1oprswap  6833  dmdcand  11969  modmul12d  13840  modnegd  13841  modadd12d  13842  exprec  14019  rpexpmord  14083  splval2  14657  dvdsmodexp  16155  eulerthlem2  16665  fermltl  16667  odzdvds  16678  fnpr2o  17453  efgredleme  19539  efgredlemc  19541  blssps  23814  blss  23815  metequiv2  23903  met1stc  23914  met2ndci  23915  metdstri  24251  xlebnum  24365  caubl  24709  divcxp  26079  cxple2a  26091  cxplead  26113  cxplt2d  26118  cxple2d  26119  mulcxpd  26120  ang180  26201  wilthlem2  26455  lgsvalmod  26701  lgsmod  26708  lgsdir2lem4  26713  lgsdirprm  26716  lgsne0  26720  lgseisen  26764  conway  27181  ax5seglem9  27949  fzm1ne1  31760  xrsmulgzz  31939  linds2eq  32241  heiborlem8  36350  cdlemd4  38737  cdleme15a  38810  cdleme17b  38823  cdleme25a  38889  cdleme25c  38891  cdleme25dN  38892  cdleme26ee  38896  tendococl  39308  tendodi1  39320  tendodi2  39321  cdlemi  39356  tendocan  39360  cdlemk5a  39371  cdlemk5  39372  cdlemk10  39379  cdlemk5u  39397  cdlemkfid1N  39457  pellexlem6  41215  acongeq  41365  jm2.25  41381  stoweidlem42  44403  stoweidlem51  44412  ldepspr  46674