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

Theorem syl133anc 1346
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl33anc.6 (𝜑𝜁)
syl133anc.7 (𝜑𝜎)
syl133anc.8 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → 𝜌)
Assertion
Ref Expression
syl133anc (𝜑𝜌)

Proof of Theorem syl133anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
6 syl33anc.6 . . 3 (𝜑𝜁)
7 syl133anc.7 . . 3 (𝜑𝜎)
85, 6, 73jca 1240 . 2 (𝜑 → (𝜂𝜁𝜎))
9 syl133anc.8 . 2 ((𝜓 ∧ (𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 8, 9syl131anc 1336 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  syl233anc  1352  mdetuni0  20359  cgrtr4d  31769  cgrtrand  31777  cgrtr3and  31779  cgrcoml  31780  cgrextendand  31793  segconeu  31795  btwnouttr2  31806  cgr3tr4  31836  cgrxfr  31839  btwnxfr  31840  lineext  31860  brofs2  31861  brifs2  31862  fscgr  31864  btwnconn1lem2  31872  btwnconn1lem4  31874  btwnconn1lem8  31878  btwnconn1lem11  31881  brsegle2  31893  seglecgr12im  31894  segletr  31898  outsidele  31916  dalem13  34477  2llnma1b  34587  cdlemblem  34594  cdlemb  34595  lhpexle3  34813  lhpat  34844  4atex2-0bOLDN  34880  cdlemd4  35003  cdleme14  35075  cdleme19b  35107  cdleme20f  35117  cdleme20j  35121  cdleme20k  35122  cdleme20l2  35124  cdleme20  35127  cdleme22a  35143  cdleme22e  35147  cdleme26e  35162  cdleme28  35176  cdleme38n  35267  cdleme41sn4aw  35278  cdleme41snaw  35279  cdlemg6c  35423  cdlemg6  35426  cdlemg8c  35432  cdlemg9  35437  cdlemg10a  35443  cdlemg12c  35448  cdlemg12d  35449  cdlemg18d  35484  cdlemg18  35485  cdlemg20  35488  cdlemg21  35489  cdlemg22  35490  cdlemg28a  35496  cdlemg33b0  35504  cdlemg28b  35506  cdlemg33a  35509  cdlemg33  35514  cdlemg34  35515  cdlemg36  35517  cdlemg38  35518  cdlemg46  35538  cdlemk6  35640  cdlemki  35644  cdlemksv2  35650  cdlemk11  35652  cdlemk6u  35665  cdleml4N  35782  cdlemn11pre  36014
  Copyright terms: Public domain W3C validator