Theorem syl221anc 1377

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  syl222anc  1382  vtocldf  3555  f1oprswap  6657  dmdcand  11444  modmul12d  13292  modnegd  13293  modadd12d  13294  exprec  13469  rpexpmord  13531  splval2  14118  dvdsmodexp  15614  eulerthlem2  16118  fermltl  16120  odzdvds  16131  fnpr2o  16829  efgredleme  18868  efgredlemc  18870  blssps  23033  blss  23034  metequiv2  23119  met1stc  23130  met2ndci  23131  metdstri  23458  xlebnum  23568  caubl  23910  divcxp  25269  cxple2a  25281  cxplead  25303  cxplt2d  25308  cxple2d  25309  mulcxpd  25310  ang180  25391  wilthlem2  25645  lgsvalmod  25891  lgsmod  25898  lgsdir2lem4  25903  lgsdirprm  25906  lgsne0  25910  lgseisen  25954  ax5seglem9  26722  fzm1ne1  30511  xrsmulgzz  30665  linds2eq  30941  conway  33264  etasslt  33274  heiborlem8  35095  cdlemd4  37336  cdleme15a  37409  cdleme17b  37422  cdleme25a  37488  cdleme25c  37490  cdleme25dN  37491  cdleme26ee  37495  tendococl  37907  tendodi1  37919  tendodi2  37920  cdlemi  37955  tendocan  37959  cdlemk5a  37970  cdlemk5  37971  cdlemk10  37978  cdlemk5u  37996  cdlemkfid1N  38056  pellexlem6  39429  acongeq  39578  jm2.25  39594  stoweidlem42  42326  stoweidlem51  42335  ldepspr  44527