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

Theorem syl123anc 1493
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 (𝜑𝜁)
syl123anc.7 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
Assertion
Ref Expression
syl123anc (𝜑𝜎)

Proof of Theorem syl123anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
42, 3jca 501 . 2 (𝜑 → (𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl123anc.7 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
91, 4, 5, 6, 7, 8syl113anc 1488 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  dvfsumlem2  24010  atbtwnexOLDN  35255  atbtwnex  35256  osumcllem7N  35770  lhpmcvr5N  35835  cdleme22f2  36156  cdlemefs32sn1aw  36223  cdlemg7aN  36434  cdlemg7N  36435  cdlemg8c  36438  cdlemg8  36440  cdlemg11aq  36447  cdlemg12b  36453  cdlemg12e  36456  cdlemg12g  36458  cdlemg13a  36460  cdlemg15a  36464  cdlemg17e  36474  cdlemg18d  36490  cdlemg19a  36492  cdlemg20  36494  cdlemg22  36496  cdlemg28a  36502  cdlemg29  36514  cdlemg44a  36540  cdlemk34  36719  cdlemn11pre  37020  dihord10  37033  dihord2pre  37035  dihmeetlem17N  37133
  Copyright terms: Public domain W3C validator