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

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

Proof of Theorem syl33anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1121 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl33anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
94, 5, 6, 7, 8syl13anc 1477 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1070
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 1072
This theorem is referenced by:  initoeu2lem2  16871  mdetunilem9  20643  mdetuni0  20644  xmetrtri  22379  bl2in  22424  blhalf  22429  blssps  22448  blss  22449  blcld  22529  methaus  22544  metdstri  22873  metdscnlem  22877  metnrmlem3  22883  xlebnum  22983  pmltpclem1  23435  colinearalglem2  26007  axlowdim  26061  ssbnd  33912  totbndbnd  33913  heiborlem6  33940  2atm  35328  lplncvrlvol2  35416  dalem19  35483  paddasslem9  35629  pclclN  35692  pclfinN  35701  pclfinclN  35751  pexmidlem8N  35778  trlval3  35989  cdleme22b  36143  cdlemefr29bpre0N  36208  cdlemefr29clN  36209  cdlemefr32fvaN  36211  cdlemefr32fva1  36212  cdlemg31b0N  36496  cdlemg31b0a  36497  cdlemh  36619  dihmeetlem16N  37125  dihmeetlem18N  37127  dihmeetlem19N  37128  dihmeetlem20N  37129  hoidmvlelem1  41323
  Copyright terms: Public domain W3C validator