MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl333anc Structured version   Visualization version   GIF version

Theorem syl333anc 1396
Description: A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl33anc.6 (𝜑𝜁)
syl133anc.7 (𝜑𝜎)
syl233anc.8 (𝜑𝜌)
syl333anc.9 (𝜑𝜇)
syl333anc.10 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ (𝜎𝜌𝜇)) → 𝜆)
Assertion
Ref Expression
syl333anc (𝜑𝜆)

Proof of Theorem syl333anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . 2 (𝜑𝜂)
6 syl33anc.6 . 2 (𝜑𝜁)
7 syl133anc.7 . . 3 (𝜑𝜎)
8 syl233anc.8 . . 3 (𝜑𝜌)
9 syl333anc.9 . . 3 (𝜑𝜇)
107, 8, 93jca 1122 . 2 (𝜑 → (𝜎𝜌𝜇))
11 syl333anc.10 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ (𝜎𝜌𝜇)) → 𝜆)
121, 2, 3, 4, 5, 6, 10, 11syl331anc 1389 1 (𝜑𝜆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081
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 1083
This theorem is referenced by:  eengtrkg  26764  ofscom  33456  cgrextend  33457  segconeq  33459  ifscgr  33493  cgrsub  33494  btwnxfr  33505  fscgr  33529  linecgr  33530  btwnconn1lem4  33539  btwnconn1lem5  33540  btwnconn1lem6  33541  btwnconn1lem8  33543  btwnconn1lem11  33546  seglecgr12  33560  colinbtwnle  33567  lshpkrlem6  36238  ps-2c  36651  pmodlem1  36969  pmodlem2  36970  dalawlem4  36997  dalawlem9  37002  4atexlemc  37192  cdleme11l  37392  cdleme15c  37399  cdleme16  37408  cdleme19e  37430  cdleme20l2  37444  cdleme20l  37445  cdleme20m  37446  cdleme20  37447  cdleme21d  37453  cdleme21e  37454  cdleme26ee  37483  cdleme26eALTN  37484  cdleme27a  37490  cdleme28b  37494  cdleme28c  37495  cdleme36m  37584  cdlemg12  37773  cdlemg16ALTN  37781  cdlemg17iqN  37797  cdlemg18c  37803  cdlemg19  37807  cdlemg21  37809  cdlemg28  37827  cdlemk11  37972  cdlemk12  37973  cdlemk16a  37979  cdlemk16  37980  cdlemk18  37991  cdlemk19  37992  cdlemk11u  37994  cdlemk12u  37995  cdlemk21N  37996  cdlemk20  37997  cdlemkoatnle-2N  37998  cdlemk13-2N  37999  cdlemkole-2N  38000  cdlemk14-2N  38001  cdlemk15-2N  38002  cdlemk16-2N  38003  cdlemk17-2N  38004  cdlemk18-2N  38009  cdlemk19-2N  38010  cdlemk7u-2N  38011  cdlemk11u-2N  38012  cdlemk12u-2N  38013  cdlemk22  38016  cdlemk30  38017  cdlemk23-3  38025  cdlemk26b-3  38028  cdlemk26-3  38029  cdlemk27-3  38030  cdlemk11ta  38052  cdlemk47  38072  dia2dimlem1  38187
  Copyright terms: Public domain W3C validator