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

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

Proof of Theorem syl333anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.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 1240 . 2 (𝜑 → (𝜎𝜌𝜇))
11 syl333anc.10 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ (𝜎𝜌𝜇)) → 𝜆)
121, 2, 3, 4, 5, 6, 10, 11syl331anc 1348 1 (𝜑𝜆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  eengtrkg  25782  ofscom  31791  cgrextend  31792  segconeq  31794  ifscgr  31828  cgrsub  31829  btwnxfr  31840  fscgr  31864  linecgr  31865  btwnconn1lem4  31874  btwnconn1lem5  31875  btwnconn1lem6  31876  btwnconn1lem8  31878  btwnconn1lem11  31881  seglecgr12  31895  colinbtwnle  31902  lshpkrlem6  33917  ps-2c  34329  pmodlem1  34647  pmodlem2  34648  dalawlem4  34675  dalawlem9  34680  4atexlemc  34870  cdleme11l  35071  cdleme15c  35078  cdleme16  35087  cdleme19e  35110  cdleme20l2  35124  cdleme20l  35125  cdleme20m  35126  cdleme20  35127  cdleme21d  35133  cdleme21e  35134  cdleme26ee  35163  cdleme26eALTN  35164  cdleme27a  35170  cdleme28b  35174  cdleme28c  35175  cdleme36m  35264  cdlemg12  35453  cdlemg16ALTN  35461  cdlemg17iqN  35477  cdlemg18c  35483  cdlemg19  35487  cdlemg21  35489  cdlemg28  35507  cdlemk11  35652  cdlemk12  35653  cdlemk16a  35659  cdlemk16  35660  cdlemk18  35671  cdlemk19  35672  cdlemk11u  35674  cdlemk12u  35675  cdlemk21N  35676  cdlemk20  35677  cdlemkoatnle-2N  35678  cdlemk13-2N  35679  cdlemkole-2N  35680  cdlemk14-2N  35681  cdlemk15-2N  35682  cdlemk16-2N  35683  cdlemk17-2N  35684  cdlemk18-2N  35689  cdlemk19-2N  35690  cdlemk7u-2N  35691  cdlemk11u-2N  35692  cdlemk12u-2N  35693  cdlemk22  35696  cdlemk30  35697  cdlemk23-3  35705  cdlemk26b-3  35708  cdlemk26-3  35709  cdlemk27-3  35710  cdlemk11ta  35732  cdlemk47  35752  dia2dimlem1  35868
  Copyright terms: Public domain W3C validator