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  3514  f1oprswap  6813  dmdcand  11933  modmul12d  13834  modnegd  13835  modadd12d  13836  exprec  14012  rpexpmord  14077  splval2  14666  dvdsmodexp  16173  eulerthlem2  16695  fermltl  16697  odzdvds  16709  fnpr2o  17463  efgredleme  19657  efgredlemc  19659  blssps  24340  blss  24341  metequiv2  24426  met1stc  24437  met2ndci  24438  metdstri  24768  xlebnum  24892  caubl  25236  divcxp  26624  cxple2a  26636  cxplead  26658  cxplt2d  26663  cxple2d  26664  mulcxpd  26665  ang180  26752  wilthlem2  27007  lgsvalmod  27255  lgsmod  27262  lgsdir2lem4  27267  lgsdirprm  27270  lgsne0  27274  lgseisen  27318  conway  27741  ax5seglem9  28917  fzm1ne1  32775  xrsmulgzz  32997  linds2eq  33353  heiborlem8  37878  cdlemd4  40320  cdleme15a  40393  cdleme17b  40406  cdleme25a  40472  cdleme25c  40474  cdleme25dN  40475  cdleme26ee  40479  tendococl  40891  tendodi1  40903  tendodi2  40904  cdlemi  40939  tendocan  40943  cdlemk5a  40954  cdlemk5  40955  cdlemk10  40962  cdlemk5u  40980  cdlemkfid1N  41040  pellexlem6  42951  acongeq  43100  jm2.25  43116  stoweidlem42  46164  stoweidlem51  46173  ldepspr  48598