Theorem syl221anc 1389

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  syl222anc  1394  vtocldf  3508  f1oprswap  6819  dmdcand  11958  modmul12d  13885  modnegd  13886  modadd12d  13887  exprec  14063  rpexpmord  14128  splval2  14717  dvdsmodexp  16227  eulerthlem2  16750  fermltl  16752  odzdvds  16764  fnpr2o  17519  efgredleme  19716  efgredlemc  19718  blssps  24414  blss  24415  metequiv2  24500  met1stc  24511  met2ndci  24512  metdstri  24842  xlebnum  24957  caubl  25300  divcxp  26676  cxple2a  26688  cxplead  26710  cxplt2d  26715  cxple2d  26716  mulcxpd  26717  ang180  26803  wilthlem2  27057  lgsvalmod  27304  lgsmod  27311  lgsdir2lem4  27316  lgsdirprm  27319  lgsne0  27323  lgseisen  27367  conway  27796  ax5seglem9  29031  fzm1ne1  32887  xrsmulgzz  33095  linds2eq  33471  heiborlem8  38192  cdlemd4  40700  cdleme15a  40773  cdleme17b  40786  cdleme25a  40852  cdleme25c  40854  cdleme25dN  40855  cdleme26ee  40859  tendococl  41271  tendodi1  41283  tendodi2  41284  cdlemi  41319  tendocan  41323  cdlemk5a  41334  cdlemk5  41335  cdlemk10  41342  cdlemk5u  41360  cdlemkfid1N  41420  pellexlem6  43286  acongeq  43435  jm2.25  43451  stoweidlem42  46492  stoweidlem51  46501  ldepspr  48971