MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl23anc Structured version   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  7646  ackbij1lem16  8105  div2subd  9830  restopn2  17231  tsmsxp  18174  blcld  18525  metustexhalfOLD  18583  metustexhalf  18584  cnllycmp  18971  dvlipcn  19868  evl1expd  19948  tanregt0  20431  ostthlem1  21311  pnfneige0  24326  qqhval2  24356  esumcocn  24460  ax5seglem6  25838  axcontlem4  25871  axcontlem7  25874  heiborlem8  26481  mpaaeu  27287  bnj1125  29262  2atjm  30143  1cvrat  30174  lvolnlelln  30282  lvolnlelpln  30283  4atlem3  30294  lplncvrlvol  30314  dalem39  30409  cdleme4a  30937  cdleme15  30976  cdleme16c  30978  cdleme19b  31002  cdleme19e  31005  cdleme20d  31010  cdleme20g  31013  cdleme20j  31016  cdleme20k  31017  cdleme20l2  31019  cdleme20l  31020  cdleme20m  31021  cdleme22e  31042  cdleme22eALTN  31043  cdleme22f  31044  cdleme27cl  31064  cdlemefr27cl  31101
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