Theorem syl221anc 1408

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl222anc  1413  vtocldf  3528  f1oprswap  6870  dmdcand  12031  modmul12d  13974  modnegd  13975  modadd12d  13976  exprec  14152  rpexpmord  14217  splval2  14811  dvdsmodexp  16335  eulerthlem2  16858  fermltl  16860  odzdvds  16872  fnpr2o  17628  efgredleme  19836  efgredlemc  19838  blssps  24610  blss  24611  metequiv2  24696  met1stc  24707  met2ndci  24708  metdstri  25038  xlebnum  25153  caubl  25496  divcxp  26881  cxple2a  26893  cxplead  26915  cxplt2d  26920  cxple2d  26921  mulcxpd  26922  ang180  27008  wilthlem2  27262  lgsvalmod  27509  lgsmod  27516  lgsdir2lem4  27521  lgsdirprm  27524  lgsne0  27528  lgseisen  27572  conway  28001  ax5seglem9  29316  fzm1ne1  33162  xrsmulgzz  33352  linds2eq  33717  heiborlem8  38502  cdlemd4  41008  cdleme15a  41081  cdleme17b  41094  cdleme25a  41160  cdleme25c  41162  cdleme25dN  41163  cdleme26ee  41167  tendococl  41579  tendodi1  41591  tendodi2  41592  cdlemi  41627  tendocan  41631  cdlemk5a  41642  cdlemk5  41643  cdlemk10  41650  cdlemk5u  41668  cdlemkfid1N  41728  pellexlem6  43594  acongeq  43743  jm2.25  43759  stoweidlem42  46789  stoweidlem51  46798  ldepspr  49286