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

Theorem syl333anc 1509
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 1123 . 2 (𝜑 → (𝜎𝜌𝜇))
11 syl333anc.10 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ (𝜎𝜌𝜇)) → 𝜆)
121, 2, 3, 4, 5, 6, 10, 11syl331anc 1502 1 (𝜑𝜆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  eengtrkg  26085  ofscom  32441  cgrextend  32442  segconeq  32444  ifscgr  32478  cgrsub  32479  btwnxfr  32490  fscgr  32514  linecgr  32515  btwnconn1lem4  32524  btwnconn1lem5  32525  btwnconn1lem6  32526  btwnconn1lem8  32528  btwnconn1lem11  32531  seglecgr12  32545  colinbtwnle  32552  lshpkrlem6  34923  ps-2c  35335  pmodlem1  35653  pmodlem2  35654  dalawlem4  35681  dalawlem9  35686  4atexlemc  35876  cdleme11l  36077  cdleme15c  36084  cdleme16  36093  cdleme19e  36115  cdleme20l2  36129  cdleme20l  36130  cdleme20m  36131  cdleme20  36132  cdleme21d  36138  cdleme21e  36139  cdleme26ee  36168  cdleme26eALTN  36169  cdleme27a  36175  cdleme28b  36179  cdleme28c  36180  cdleme36m  36269  cdlemg12  36458  cdlemg16ALTN  36466  cdlemg17iqN  36482  cdlemg18c  36488  cdlemg19  36492  cdlemg21  36494  cdlemg28  36512  cdlemk11  36657  cdlemk12  36658  cdlemk16a  36664  cdlemk16  36665  cdlemk18  36676  cdlemk19  36677  cdlemk11u  36679  cdlemk12u  36680  cdlemk21N  36681  cdlemk20  36682  cdlemkoatnle-2N  36683  cdlemk13-2N  36684  cdlemkole-2N  36685  cdlemk14-2N  36686  cdlemk15-2N  36687  cdlemk16-2N  36688  cdlemk17-2N  36689  cdlemk18-2N  36694  cdlemk19-2N  36695  cdlemk7u-2N  36696  cdlemk11u-2N  36697  cdlemk12u-2N  36698  cdlemk22  36701  cdlemk30  36702  cdlemk23-3  36710  cdlemk26b-3  36713  cdlemk26-3  36714  cdlemk27-3  36715  cdlemk11ta  36737  cdlemk47  36757  dia2dimlem1  36873
  Copyright terms: Public domain W3C validator