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  3526  f1oprswap  6844  dmdcand  11987  modmul12d  13890  modnegd  13891  modadd12d  13892  exprec  14068  rpexpmord  14133  splval2  14722  dvdsmodexp  16230  eulerthlem2  16752  fermltl  16754  odzdvds  16766  fnpr2o  17520  efgredleme  19673  efgredlemc  19675  blssps  24312  blss  24313  metequiv2  24398  met1stc  24409  met2ndci  24410  metdstri  24740  xlebnum  24864  caubl  25208  divcxp  26596  cxple2a  26608  cxplead  26630  cxplt2d  26635  cxple2d  26636  mulcxpd  26637  ang180  26724  wilthlem2  26979  lgsvalmod  27227  lgsmod  27234  lgsdir2lem4  27239  lgsdirprm  27242  lgsne0  27246  lgseisen  27290  conway  27711  ax5seglem9  28864  fzm1ne1  32711  xrsmulgzz  32947  linds2eq  33352  heiborlem8  37812  cdlemd4  40195  cdleme15a  40268  cdleme17b  40281  cdleme25a  40347  cdleme25c  40349  cdleme25dN  40350  cdleme26ee  40354  tendococl  40766  tendodi1  40778  tendodi2  40779  cdlemi  40814  tendocan  40818  cdlemk5a  40829  cdlemk5  40830  cdlemk10  40837  cdlemk5u  40855  cdlemkfid1N  40915  pellexlem6  42822  acongeq  42972  jm2.25  42988  stoweidlem42  46040  stoweidlem51  46049  ldepspr  48462