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

Theorem syl133anc 1505
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 1151 . 2 (𝜑 → (𝜂𝜁𝜎))
9 syl133anc.8 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 8, 9syl131anc 1495 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  syl233anc  1511  mdetuni0  20659  frgrwopreg  27521  cgrtr4d  32435  cgrtrand  32443  cgrtr3and  32445  cgrcoml  32446  cgrextendand  32459  segconeu  32461  btwnouttr2  32472  cgr3tr4  32502  cgrxfr  32505  btwnxfr  32506  lineext  32526  brofs2  32527  brifs2  32528  fscgr  32530  btwnconn1lem2  32538  btwnconn1lem4  32540  btwnconn1lem8  32544  btwnconn1lem11  32547  brsegle2  32559  seglecgr12im  32560  segletr  32564  outsidele  32582  dalem13  35475  2llnma1b  35585  cdlemblem  35592  cdlemb  35593  lhpexle3  35811  lhpat  35842  4atex2-0bOLDN  35878  cdlemd4  36000  cdleme14  36072  cdleme19b  36103  cdleme20f  36113  cdleme20j  36117  cdleme20k  36118  cdleme20l2  36120  cdleme20  36123  cdleme22a  36139  cdleme22e  36143  cdleme26e  36158  cdleme28  36172  cdleme38n  36263  cdleme41sn4aw  36274  cdleme41snaw  36275  cdlemg6c  36419  cdlemg6  36422  cdlemg8c  36428  cdlemg9  36433  cdlemg10a  36439  cdlemg12c  36444  cdlemg12d  36445  cdlemg18d  36480  cdlemg18  36481  cdlemg20  36484  cdlemg21  36485  cdlemg22  36486  cdlemg28a  36492  cdlemg33b0  36500  cdlemg28b  36502  cdlemg33a  36505  cdlemg33  36510  cdlemg34  36511  cdlemg36  36513  cdlemg38  36514  cdlemg46  36534  cdlemk6  36636  cdlemki  36640  cdlemksv2  36646  cdlemk11  36648  cdlemk6u  36661  cdleml4N  36778  cdlemn11pre  37009
  Copyright terms: Public domain W3C validator