Theorem syl221anc 1384

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 1379	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  syl222anc  1389  vtocldf  3519  f1oprswap  6827  dmdcand  11958  modmul12d  13860  modnegd  13861  modadd12d  13862  exprec  14038  rpexpmord  14103  splval2  14692  dvdsmodexp  16199  eulerthlem2  16721  fermltl  16723  odzdvds  16735  fnpr2o  17490  efgredleme  19684  efgredlemc  19686  blssps  24380  blss  24381  metequiv2  24466  met1stc  24477  met2ndci  24478  metdstri  24808  xlebnum  24932  caubl  25276  divcxp  26664  cxple2a  26676  cxplead  26698  cxplt2d  26703  cxple2d  26704  mulcxpd  26705  ang180  26792  wilthlem2  27047  lgsvalmod  27295  lgsmod  27302  lgsdir2lem4  27307  lgsdirprm  27310  lgsne0  27314  lgseisen  27358  conway  27787  ax5seglem9  29022  fzm1ne1  32878  xrsmulgzz  33101  linds2eq  33473  heiborlem8  38063  cdlemd4  40571  cdleme15a  40644  cdleme17b  40657  cdleme25a  40723  cdleme25c  40725  cdleme25dN  40726  cdleme26ee  40730  tendococl  41142  tendodi1  41154  tendodi2  41155  cdlemi  41190  tendocan  41194  cdlemk5a  41205  cdlemk5  41206  cdlemk10  41213  cdlemk5u  41231  cdlemkfid1N  41291  pellexlem6  43185  acongeq  43334  jm2.25  43350  stoweidlem42  46394  stoweidlem51  46403  ldepspr  48827