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  7402  ackbij1lem16  7861  div2subd  9586  restopn2  16908  tsmsxp  17837  blcld  18051  cnllycmp  18454  dvlipcn  19341  evl1expd  19421  tanregt0  19901  ostthlem1  20776  pnfneige0  23374  esumcocn  23448  brbtwn2  24533  ax5seglem6  24562  axcontlem4  24595  axcontlem7  24598  heiborlem8  26542  mpaaeu  27355  bnj1125  29022  2atjm  29634  1cvrat  29665  lvolnlelln  29773  lvolnlelpln  29774  4atlem3  29785  lplncvrlvol  29805  dalem39  29900  cdleme4a  30428  cdleme15  30467  cdleme16c  30469  cdleme19b  30493  cdleme19e  30496  cdleme20d  30501  cdleme20g  30504  cdleme20j  30507  cdleme20k  30508  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme22e  30533  cdleme22eALTN  30534  cdleme22f  30535  cdleme27cl  30555  cdlemefr27cl  30592
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