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

Theorem syl133anc 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 (𝜑𝜂)
syl33anc.6 (𝜑𝜁)
syl133anc.7 (𝜑𝜎)
syl133anc.8 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → 𝜌)
Assertion
Ref Expression
syl133anc (𝜑𝜌)

Proof of Theorem syl133anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
6 syl33anc.6 . . 3 (𝜑𝜁)
7 syl133anc.7 . . 3 (𝜑𝜎)
85, 6, 73jca 1124 . 2 (𝜑 → (𝜂𝜁𝜎))
9 syl133anc.8 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 8, 9syl131anc 1379 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1083
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 1085
This theorem is referenced by:  syl233anc  1395  mdetuni0  21229  frgrwopreg  28101  cgrtr4d  33446  cgrtrand  33454  cgrtr3and  33456  cgrcoml  33457  cgrextendand  33470  segconeu  33472  btwnouttr2  33483  cgr3tr4  33513  cgrxfr  33516  btwnxfr  33517  lineext  33537  brofs2  33538  brifs2  33539  fscgr  33541  btwnconn1lem2  33549  btwnconn1lem4  33551  btwnconn1lem8  33555  btwnconn1lem11  33558  brsegle2  33570  seglecgr12im  33571  segletr  33575  outsidele  33593  dalem13  36811  2llnma1b  36921  cdlemblem  36928  cdlemb  36929  lhpexle3  37147  lhpat  37178  4atex2-0bOLDN  37214  cdlemd4  37336  cdleme14  37408  cdleme19b  37439  cdleme20f  37449  cdleme20j  37453  cdleme20k  37454  cdleme20l2  37456  cdleme20  37459  cdleme22a  37475  cdleme22e  37479  cdleme26e  37494  cdleme28  37508  cdleme38n  37599  cdleme41sn4aw  37610  cdleme41snaw  37611  cdlemg6c  37755  cdlemg6  37758  cdlemg8c  37764  cdlemg9  37769  cdlemg10a  37775  cdlemg12c  37780  cdlemg12d  37781  cdlemg18d  37816  cdlemg18  37817  cdlemg20  37820  cdlemg21  37821  cdlemg22  37822  cdlemg28a  37828  cdlemg33b0  37836  cdlemg28b  37838  cdlemg33a  37841  cdlemg33  37846  cdlemg34  37847  cdlemg36  37849  cdlemg38  37850  cdlemg46  37870  cdlemk6  37972  cdlemki  37976  cdlemksv2  37982  cdlemk11  37984  cdlemk6u  37997  cdleml4N  38114  cdlemn11pre  38345
  Copyright terms: Public domain W3C validator