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

Theorem syl133anc 1393
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 1128 . 2 (𝜑 → (𝜂𝜁𝜎))
9 syl133anc.8 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 8, 9syl131anc 1383 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 206  df-an 398  df-3an 1089
This theorem is referenced by:  syl233anc  1399  mdetuni0  21819  frgrwopreg  28736  cgrtr4d  34336  cgrtrand  34344  cgrtr3and  34346  cgrcoml  34347  cgrextendand  34360  segconeu  34362  btwnouttr2  34373  cgr3tr4  34403  cgrxfr  34406  btwnxfr  34407  lineext  34427  brofs2  34428  brifs2  34429  fscgr  34431  btwnconn1lem2  34439  btwnconn1lem4  34441  btwnconn1lem8  34445  btwnconn1lem11  34448  brsegle2  34460  seglecgr12im  34461  segletr  34465  outsidele  34483  dalem13  37890  2llnma1b  38000  cdlemblem  38007  cdlemb  38008  lhpexle3  38226  lhpat  38257  4atex2-0bOLDN  38293  cdlemd4  38415  cdleme14  38487  cdleme19b  38518  cdleme20f  38528  cdleme20j  38532  cdleme20k  38533  cdleme20l2  38535  cdleme20  38538  cdleme22a  38554  cdleme22e  38558  cdleme26e  38573  cdleme28  38587  cdleme38n  38678  cdleme41sn4aw  38689  cdleme41snaw  38690  cdlemg6c  38834  cdlemg6  38837  cdlemg8c  38843  cdlemg9  38848  cdlemg10a  38854  cdlemg12c  38859  cdlemg12d  38860  cdlemg18d  38895  cdlemg18  38896  cdlemg20  38899  cdlemg21  38900  cdlemg22  38901  cdlemg28a  38907  cdlemg33b0  38915  cdlemg28b  38917  cdlemg33a  38920  cdlemg33  38925  cdlemg34  38926  cdlemg36  38928  cdlemg38  38929  cdlemg46  38949  cdlemk6  39051  cdlemki  39055  cdlemksv2  39061  cdlemk11  39063  cdlemk6u  39076  cdleml4N  39193  cdlemn11pre  39424
  Copyright terms: Public domain W3C validator