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

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

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 1105

This theorem is referenced by:  syl222anc  1413  vtocldf  3527  f1oprswap  6868  dmdcand  12021  modmul12d  13963  modnegd  13964  modadd12d  13965  exprec  14141  rpexpmord  14206  splval2  14796  dvdsmodexp  16319  eulerthlem2  16842  fermltl  16844  odzdvds  16856  fnpr2o  17612  efgredleme  19814  efgredlemc  19816  blssps  24562  blss  24563  metequiv2  24648  met1stc  24659  met2ndci  24660  metdstri  24990  xlebnum  25105  caubl  25448  divcxp  26833  cxple2a  26845  cxplead  26867  cxplt2d  26872  cxple2d  26873  mulcxpd  26874  ang180  26960  wilthlem2  27214  lgsvalmod  27461  lgsmod  27468  lgsdir2lem4  27473  lgsdirprm  27476  lgsne0  27480  lgseisen  27524  conway  27953  ax5seglem9  29268  fzm1ne1  33114  xrsmulgzz  33310  linds2eq  33675  heiborlem8  38450  cdlemd4  40956  cdleme15a  41029  cdleme17b  41042  cdleme25a  41108  cdleme25c  41110  cdleme25dN  41111  cdleme26ee  41115  tendococl  41527  tendodi1  41539  tendodi2  41540  cdlemi  41575  tendocan  41579  cdlemk5a  41590  cdlemk5  41591  cdlemk10  41598  cdlemk5u  41616  cdlemkfid1N  41676  pellexlem6  43544  acongeq  43693  jm2.25  43709  stoweidlem42  46739  stoweidlem51  46748  ldepspr  49236