Theorem syl221anc 1383

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 1378	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  1388  vtocldf  3515  f1oprswap  6816  dmdcand  11936  modmul12d  13842  modnegd  13843  modadd12d  13844  exprec  14020  rpexpmord  14085  splval2  14674  dvdsmodexp  16181  eulerthlem2  16703  fermltl  16705  odzdvds  16717  fnpr2o  17471  efgredleme  19665  efgredlemc  19667  blssps  24349  blss  24350  metequiv2  24435  met1stc  24446  met2ndci  24447  metdstri  24777  xlebnum  24901  caubl  25245  divcxp  26633  cxple2a  26645  cxplead  26667  cxplt2d  26672  cxple2d  26673  mulcxpd  26674  ang180  26761  wilthlem2  27016  lgsvalmod  27264  lgsmod  27271  lgsdir2lem4  27276  lgsdirprm  27279  lgsne0  27283  lgseisen  27327  conway  27750  ax5seglem9  28926  fzm1ne1  32782  xrsmulgzz  33001  linds2eq  33357  heiborlem8  37868  cdlemd4  40310  cdleme15a  40383  cdleme17b  40396  cdleme25a  40462  cdleme25c  40464  cdleme25dN  40465  cdleme26ee  40469  tendococl  40881  tendodi1  40893  tendodi2  40894  cdlemi  40929  tendocan  40933  cdlemk5a  40944  cdlemk5  40945  cdlemk10  40952  cdlemk5u  40970  cdlemkfid1N  41030  pellexlem6  42941  acongeq  43090  jm2.25  43106  stoweidlem42  46154  stoweidlem51  46163  ldepspr  48588