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

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

Proof of Theorem syl123anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
42, 3jca 510 . 2 (𝜑 → (𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl123anc.7 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
91, 4, 5, 6, 7, 8syl113anc 1380 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1085
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 395  df-3an 1087
This theorem is referenced by:  dvfsumlem2  25779  noinfbnd2  27470  gg-dvfsumlem2  35469  atbtwnexOLDN  38621  atbtwnex  38622  osumcllem7N  39136  lhpmcvr5N  39201  cdleme22f2  39521  cdlemefs32sn1aw  39588  cdlemg7aN  39799  cdlemg7N  39800  cdlemg8c  39803  cdlemg8  39805  cdlemg11aq  39812  cdlemg12b  39818  cdlemg12e  39821  cdlemg12g  39823  cdlemg13a  39825  cdlemg15a  39829  cdlemg17e  39839  cdlemg18d  39855  cdlemg19a  39857  cdlemg20  39859  cdlemg22  39861  cdlemg28a  39867  cdlemg29  39879  cdlemg44a  39905  cdlemk34  40084  cdlemn11pre  40384  dihord10  40397  dihord2pre  40399  dihmeetlem17N  40497
  Copyright terms: Public domain W3C validator