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

Theorem simp3rl 1064
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 1014 1  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 970
This theorem is referenced by:  omeu  7224  hashbclem  12454  tsmsxp  20385  tgqioo  21033  ovolunlem2  21637  plyadd  22342  plymul  22343  coeeu  22350  tghilbert1_2  23725  gxmul  24942  cvmlift2lem10  28383  ntrivcvgmul  28599  btwnconn1lem1  29300  btwnconn1lem2  29301  btwnconn1lem12  29311  jm2.27  30543  lplnexllnN  34235  2llnjN  34238  4atlem12b  34282  lplncvrlvol2  34286  lncmp  34454  cdlema2N  34463  cdlemc2  34863  cdleme11a  34931  cdleme22eALTN  35016  cdleme24  35023  cdleme27a  35038  cdleme27N  35040  cdleme28  35044  cdlemefs29bpre0N  35087  cdlemefs29bpre1N  35088  cdlemefs29cpre1N  35089  cdlemefs29clN  35090  cdlemefs32fvaN  35093  cdlemefs32fva1  35094  cdleme36m  35132  cdleme39a  35136  cdleme17d3  35167  cdleme50trn2  35222  cdlemg36  35385  cdlemj3  35494  cdlemkfid1N  35592  cdlemkid1  35593  cdlemk19ylem  35601  cdlemk19xlem  35613  dihlsscpre  35906  dihord4  35930  dihatlat  36006  mapdh9a  36462
  Copyright terms: Public domain W3C validator