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

Theorem syl333anc 1401
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 1127 . 2 (𝜑 → (𝜎𝜌𝜇))
11 syl333anc.10 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ (𝜎𝜌𝜇)) → 𝜆)
121, 2, 3, 4, 5, 6, 10, 11syl331anc 1394 1 (𝜑𝜆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  eengtrkg  29015  ofscom  35988  cgrextend  35989  segconeq  35991  ifscgr  36025  cgrsub  36026  btwnxfr  36037  fscgr  36061  linecgr  36062  btwnconn1lem4  36071  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem8  36075  btwnconn1lem11  36078  seglecgr12  36092  colinbtwnle  36099  lshpkrlem6  39096  ps-2c  39510  pmodlem1  39828  pmodlem2  39829  dalawlem4  39856  dalawlem9  39861  4atexlemc  40051  cdleme11l  40251  cdleme15c  40258  cdleme16  40267  cdleme19e  40289  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme20  40306  cdleme21d  40312  cdleme21e  40313  cdleme26ee  40342  cdleme26eALTN  40343  cdleme27a  40349  cdleme28b  40353  cdleme28c  40354  cdleme36m  40443  cdlemg12  40632  cdlemg16ALTN  40640  cdlemg17iqN  40656  cdlemg18c  40662  cdlemg19  40666  cdlemg21  40668  cdlemg28  40686  cdlemk11  40831  cdlemk12  40832  cdlemk16a  40838  cdlemk16  40839  cdlemk18  40850  cdlemk19  40851  cdlemk11u  40853  cdlemk12u  40854  cdlemk21N  40855  cdlemk20  40856  cdlemkoatnle-2N  40857  cdlemk13-2N  40858  cdlemkole-2N  40859  cdlemk14-2N  40860  cdlemk15-2N  40861  cdlemk16-2N  40862  cdlemk17-2N  40863  cdlemk18-2N  40868  cdlemk19-2N  40869  cdlemk7u-2N  40870  cdlemk11u-2N  40871  cdlemk12u-2N  40872  cdlemk22  40875  cdlemk30  40876  cdlemk23-3  40884  cdlemk26b-3  40887  cdlemk26-3  40888  cdlemk27-3  40889  cdlemk11ta  40911  cdlemk47  40931  dia2dimlem1  41046
  Copyright terms: Public domain W3C validator