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

Theorem syl23anc 1239
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
sylXanc.5  |-  ( ph  ->  et )
syl23anc.6  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta  /\  et ) )  ->  ze )
Assertion
Ref Expression
syl23anc  |-  ( ph  ->  ze )

Proof of Theorem syl23anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 532 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 sylXanc.3 . 2  |-  ( ph  ->  th )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 sylXanc.5 . 2  |-  ( ph  ->  et )
7 syl23anc.6 . 2  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta  /\  et ) )  ->  ze )
83, 4, 5, 6, 7syl13anc 1234 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  suppofss1d  6942  suppofss2d  6943  cnfcomlem  8177  cnfcomlemOLD  8185  ackbij1lem16  8649  div2subd  10413  symg2bas  16749  evl1expd  18703  psgndiflemA  18937  oftpos  19248  restopn2  19973  tsmsxp  20951  blcld  21302  metustexhalfOLD  21360  metustexhalf  21361  cnllycmp  21750  dvlipcn  22689  tanregt0  23220  ostthlem1  24195  ax5seglem6  24666  axcontlem4  24699  axcontlem7  24702  wwlkextwrd  25157  pnfneige0  28399  qqhval2  28428  esumcocn  28540  carsgmon  28775  bnj1125  29388  heiborlem8  31609  2atjm  32475  1cvrat  32506  lvolnlelln  32614  lvolnlelpln  32615  4atlem3  32626  lplncvrlvol  32646  dalem39  32741  cdleme4a  33270  cdleme15  33309  cdleme16c  33311  cdleme19b  33336  cdleme19e  33339  cdleme20d  33344  cdleme20g  33347  cdleme20j  33350  cdleme20k  33351  cdleme20l2  33353  cdleme20l  33354  cdleme20m  33355  cdleme22e  33376  cdleme22eALTN  33377  cdleme22f  33378  cdleme27cl  33398  cdlemefr27cl  33435  mpaaeu  35476
  Copyright terms: Public domain W3C validator