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

Theorem syl23anc 1272
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 535 . 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 1267 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  suppofss1d  6961  suppofss2d  6962  cnfcomlem  8207  ackbij1lem16  8667  div2subd  10435  symg2bas  17032  evl1expd  18926  psgndiflemA  19161  oftpos  19469  restopn2  20185  tsmsxp  21161  blcld  21512  metustexhalf  21563  cnllycmp  21976  dvlipcn  22938  tanregt0  23480  ostthlem1  24457  ax5seglem6  24956  axcontlem4  24989  axcontlem7  24992  wwlkextwrd  25448  pnfneige0  28759  qqhval2  28788  esumcocn  28903  carsgmon  29148  bnj1125  29803  heiborlem8  32070  2atjm  32935  1cvrat  32966  lvolnlelln  33074  lvolnlelpln  33075  4atlem3  33086  lplncvrlvol  33106  dalem39  33201  cdleme4a  33730  cdleme15  33769  cdleme16c  33771  cdleme19b  33796  cdleme19e  33799  cdleme20d  33804  cdleme20g  33807  cdleme20j  33810  cdleme20k  33811  cdleme20l2  33813  cdleme20l  33814  cdleme20m  33815  cdleme22e  33836  cdleme22eALTN  33837  cdleme22f  33838  cdleme27cl  33858  cdlemefr27cl  33895  mpaaeu  35942
  Copyright terms: Public domain W3C validator