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

Theorem syl23anc 1189
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 518 . 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 1184 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  cnfcomlem  7418  ackbij1lem16  7877  div2subd  9602  restopn2  16924  tsmsxp  17853  blcld  18067  cnllycmp  18470  dvlipcn  19357  evl1expd  19437  tanregt0  19917  ostthlem1  20792  pnfneige0  23389  esumcocn  23463  brbtwn2  24605  ax5seglem6  24634  axcontlem4  24667  axcontlem7  24670  heiborlem8  26645  mpaaeu  27458  bnj1125  29338  2atjm  30256  1cvrat  30287  lvolnlelln  30395  lvolnlelpln  30396  4atlem3  30407  lplncvrlvol  30427  dalem39  30522  cdleme4a  31050  cdleme15  31089  cdleme16c  31091  cdleme19b  31115  cdleme19e  31118  cdleme20d  31123  cdleme20g  31126  cdleme20j  31129  cdleme20k  31130  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f  31157  cdleme27cl  31177  cdlemefr27cl  31214
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator