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

Theorem syl123anc 1340
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 554 . 2 (𝜑 → (𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl123anc.7 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
91, 4, 5, 6, 7, 8syl113anc 1335 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  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:  dvfsumlem2  23701  atbtwnexOLDN  34234  atbtwnex  34235  osumcllem7N  34749  lhpmcvr5N  34814  cdleme22f2  35136  cdlemefs32sn1aw  35203  cdlemg7aN  35414  cdlemg7N  35415  cdlemg8c  35418  cdlemg8  35420  cdlemg11aq  35427  cdlemg12b  35433  cdlemg12e  35436  cdlemg12g  35438  cdlemg13a  35440  cdlemg15a  35444  cdlemg17e  35454  cdlemg18d  35470  cdlemg19a  35472  cdlemg20  35474  cdlemg22  35476  cdlemg28a  35482  cdlemg29  35494  cdlemg44a  35520  cdlemk34  35699  cdlemn11pre  36000  dihord10  36013  dihord2pre  36015  dihmeetlem17N  36113
  Copyright terms: Public domain W3C validator