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

Theorem simp3rl 1061
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp3rl  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ph )

Proof of Theorem simp3rl
StepHypRef Expression
1 simprl 755 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant3 1011 1  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  omeu  7024  hashbclem  12205  tsmsxp  19729  tgqioo  20377  ovolunlem2  20981  plyadd  21685  plymul  21686  coeeu  21693  tghilbert1_2  23044  gxmul  23765  cvmlift2lem10  27201  ntrivcvgmul  27417  btwnconn1lem1  28118  btwnconn1lem2  28119  btwnconn1lem12  28129  jm2.27  29357  lplnexllnN  33208  2llnjN  33211  4atlem12b  33255  lplncvrlvol2  33259  lncmp  33427  cdlema2N  33436  cdlemc2  33836  cdleme11a  33904  cdleme22eALTN  33989  cdleme24  33996  cdleme27a  34011  cdleme27N  34013  cdleme28  34017  cdlemefs29bpre0N  34060  cdlemefs29bpre1N  34061  cdlemefs29cpre1N  34062  cdlemefs29clN  34063  cdlemefs32fvaN  34066  cdlemefs32fva1  34067  cdleme36m  34105  cdleme39a  34109  cdleme17d3  34140  cdleme50trn2  34195  cdlemg36  34358  cdlemj3  34467  cdlemkfid1N  34565  cdlemkid1  34566  cdlemk19ylem  34574  cdlemk19xlem  34586  dihlsscpre  34879  dihord4  34903  dihatlat  34979  mapdh9a  35435
  Copyright terms: Public domain W3C validator