Theorem syl221anc 1404

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl222anc  1409  vtocldf  3529  f1oprswap  6856  dmdcand  12008  modmul12d  13949  modnegd  13950  modadd12d  13951  exprec  14127  rpexpmord  14192  splval2  14782  dvdsmodexp  16306  eulerthlem2  16829  fermltl  16831  odzdvds  16843  fnpr2o  17599  efgredleme  19801  efgredlemc  19803  blssps  24538  blss  24539  metequiv2  24624  met1stc  24635  met2ndci  24636  metdstri  24966  xlebnum  25081  caubl  25424  divcxp  26806  cxple2a  26818  cxplead  26840  cxplt2d  26845  cxple2d  26846  mulcxpd  26847  ang180  26933  wilthlem2  27187  lgsvalmod  27434  lgsmod  27441  lgsdir2lem4  27446  lgsdirprm  27449  lgsne0  27453  lgseisen  27497  conway  27926  ax5seglem9  29192  fzm1ne1  33041  xrsmulgzz  33237  linds2eq  33605  heiborlem8  38324  cdlemd4  40832  cdleme15a  40905  cdleme17b  40918  cdleme25a  40984  cdleme25c  40986  cdleme25dN  40987  cdleme26ee  40991  tendococl  41403  tendodi1  41415  tendodi2  41416  cdlemi  41451  tendocan  41455  cdlemk5a  41466  cdlemk5  41467  cdlemk10  41474  cdlemk5u  41492  cdlemkfid1N  41552  pellexlem6  43418  acongeq  43567  jm2.25  43583  stoweidlem42  46615  stoweidlem51  46624  ldepspr  49105