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

Theorem syl23anc 1373
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl23anc.6 (((𝜓𝜒) ∧ (𝜃𝜏𝜂)) → 𝜁)
Assertion
Ref Expression
syl23anc (𝜑𝜁)

Proof of Theorem syl23anc
StepHypRef Expression
1 syl3anc.1 . . 3 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
31, 2jca 514 . 2 (𝜑 → (𝜓𝜒))
4 syl3anc.3 . 2 (𝜑𝜃)
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl23anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏𝜂)) → 𝜁)
83, 4, 5, 6, 7syl13anc 1368 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  suppofss1d  7846  suppofss2d  7847  cnfcomlem  9140  ackbij1lem16  9635  div2subd  11444  symg2bas  18500  evl1expd  20484  psgndiflemA  20721  oftpos  21037  restopn2  21761  tsmsxp  22739  blcld  23091  cnllycmp  23540  dvlipcn  24576  tanregt0  25110  ostthlem1  26190  ax5seglem6  26707  axcontlem4  26740  axcontlem7  26743  wwlksnextwrd  27662  lindsunlem  31031  pnfneige0  31202  qqhval2  31231  esumcocn  31347  carsgmon  31580  bnj1125  32272  nosupbnd1lem1  33216  nosupbnd2  33224  heiborlem8  35132  2atjm  36617  1cvrat  36648  lvolnlelln  36756  lvolnlelpln  36757  4atlem3  36768  lplncvrlvol  36788  dalem39  36883  cdleme4a  37411  cdleme15  37450  cdleme16c  37452  cdleme19b  37476  cdleme19e  37479  cdleme20d  37484  cdleme20g  37487  cdleme20j  37490  cdleme20k  37491  cdleme20l2  37493  cdleme20l  37494  cdleme20m  37495  cdleme22e  37516  cdleme22eALTN  37517  cdleme22f  37518  cdleme27cl  37538  cdlemefr27cl  37575  mpaaeu  39887
  Copyright terms: Public domain W3C validator