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  3517  f1oprswap  6819  dmdcand  11946  modmul12d  13848  modnegd  13849  modadd12d  13850  exprec  14026  rpexpmord  14091  splval2  14680  dvdsmodexp  16187  eulerthlem2  16709  fermltl  16711  odzdvds  16723  fnpr2o  17478  efgredleme  19672  efgredlemc  19674  blssps  24368  blss  24369  metequiv2  24454  met1stc  24465  met2ndci  24466  metdstri  24796  xlebnum  24920  caubl  25264  divcxp  26652  cxple2a  26664  cxplead  26686  cxplt2d  26691  cxple2d  26692  mulcxpd  26693  ang180  26780  wilthlem2  27035  lgsvalmod  27283  lgsmod  27290  lgsdir2lem4  27295  lgsdirprm  27298  lgsne0  27302  lgseisen  27346  conway  27775  ax5seglem9  29010  fzm1ne1  32868  xrsmulgzz  33091  linds2eq  33462  heiborlem8  38015  cdlemd4  40457  cdleme15a  40530  cdleme17b  40543  cdleme25a  40609  cdleme25c  40611  cdleme25dN  40612  cdleme26ee  40616  tendococl  41028  tendodi1  41040  tendodi2  41041  cdlemi  41076  tendocan  41080  cdlemk5a  41091  cdlemk5  41092  cdlemk10  41099  cdlemk5u  41117  cdlemkfid1N  41177  pellexlem6  43072  acongeq  43221  jm2.25  43237  stoweidlem42  46282  stoweidlem51  46291  ldepspr  48715