Theorem syl221anc 1500

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1107

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 198  df-an 385  df-3an 1109

This theorem is referenced by:  syl222anc  1505  vtocldf  3408  f1oprswap  6363  dmdcand  11084  modmul12d  12932  modnegd  12933  modadd12d  12934  exprec  13108  splval2  13780  splval2OLD  13781  dvdsmodexp  15273  eulerthlem2  15766  fermltl  15768  odzdvds  15779  efgredleme  18421  efgredlemc  18423  blssps  22508  blss  22509  metequiv2  22594  met1stc  22605  met2ndci  22606  metdstri  22933  xlebnum  23043  caubl  23385  divcxp  24724  cxple2a  24736  cxplead  24758  cxplt2d  24763  cxple2d  24764  mulcxpd  24765  ang180  24835  wilthlem2  25086  lgsvalmod  25332  lgsmod  25339  lgsdir2lem4  25344  lgsdirprm  25347  lgsne0  25351  lgseisen  25395  ax5seglem9  26108  xrsmulgzz  30125  conway  32354  etasslt  32364  heiborlem8  34039  cdlemd4  36157  cdleme15a  36230  cdleme17b  36243  cdleme25a  36309  cdleme25c  36311  cdleme25dN  36312  cdleme26ee  36316  tendococl  36728  tendodi1  36740  tendodi2  36741  cdlemi  36776  tendocan  36780  cdlemk5a  36791  cdlemk5  36792  cdlemk10  36799  cdlemk5u  36817  cdlemkfid1N  36877  pellexlem6  38076  rpexpmord  38190  acongeq  38227  jm2.25  38243  stoweidlem42  40896  stoweidlem51  40905  ldepspr  42931