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

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

Proof of Theorem syl23anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
31, 2jca 501 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl23anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏𝜂)) → 𝜁)
83, 4, 5, 6, 7syl13anc 1478 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:  suppofss1d  7487  suppofss2d  7488  cnfcomlem  8763  ackbij1lem16  9262  div2subd  11056  symg2bas  18024  evl1expd  19923  psgndiflemA  20162  oftpos  20475  restopn2  21201  tsmsxp  22177  blcld  22529  metustexhalf  22580  cnllycmp  22974  dvlipcn  23976  tanregt0  24505  ostthlem1  25536  ax5seglem6  26034  axcontlem4  26067  axcontlem7  26070  wwlksnextwrd  27040  pnfneige0  30336  qqhval2  30365  esumcocn  30481  carsgmon  30715  bnj1125  31397  nosupbnd1lem1  32190  nosupbnd2  32198  heiborlem8  33948  2atjm  35253  1cvrat  35284  lvolnlelln  35392  lvolnlelpln  35393  4atlem3  35404  lplncvrlvol  35424  dalem39  35519  cdleme4a  36048  cdleme15  36087  cdleme16c  36089  cdleme19b  36113  cdleme19e  36116  cdleme20d  36121  cdleme20g  36124  cdleme20j  36127  cdleme20k  36128  cdleme20l2  36130  cdleme20l  36131  cdleme20m  36132  cdleme22e  36153  cdleme22eALTN  36154  cdleme22f  36155  cdleme27cl  36175  cdlemefr27cl  36212  mpaaeu  38246
  Copyright terms: Public domain W3C validator