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

Theorem syl23anc 1191
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 519 . 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 1186 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  cnfcomlem  7590  ackbij1lem16  8049  div2subd  9773  restopn2  17164  tsmsxp  18106  blcld  18426  metustexhalf  18477  cnllycmp  18853  dvlipcn  19746  evl1expd  19826  tanregt0  20309  ostthlem1  21189  pnfneige0  24141  qqhval2  24166  esumcocn  24267  ax5seglem6  25588  axcontlem4  25621  axcontlem7  25624  heiborlem8  26219  mpaaeu  27025  bnj1125  28700  2atjm  29560  1cvrat  29591  lvolnlelln  29699  lvolnlelpln  29700  4atlem3  29711  lplncvrlvol  29731  dalem39  29826  cdleme4a  30354  cdleme15  30393  cdleme16c  30395  cdleme19b  30419  cdleme19e  30422  cdleme20d  30427  cdleme20g  30430  cdleme20j  30433  cdleme20k  30434  cdleme20l2  30436  cdleme20l  30437  cdleme20m  30438  cdleme22e  30459  cdleme22eALTN  30460  cdleme22f  30461  cdleme27cl  30481  cdlemefr27cl  30518
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator