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

Theorem simp3rl 1068
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 1018 1  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 972
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 974
This theorem is referenced by:  omeu  7232  hashbclem  12475  tsmsxp  20523  tgqioo  21171  ovolunlem2  21775  plyadd  22480  plymul  22481  coeeu  22488  tghilbert1_2  23883  gxmul  25145  cvmlift2lem10  28623  ntrivcvgmul  29004  btwnconn1lem1  29705  btwnconn1lem2  29706  btwnconn1lem12  29716  jm2.27  30918  lplnexllnN  34990  2llnjN  34993  4atlem12b  35037  lplncvrlvol2  35041  lncmp  35209  cdlema2N  35218  cdlemc2  35619  cdleme11a  35687  cdleme22eALTN  35773  cdleme24  35780  cdleme27a  35795  cdleme27N  35797  cdleme28  35801  cdlemefs29bpre0N  35844  cdlemefs29bpre1N  35845  cdlemefs29cpre1N  35846  cdlemefs29clN  35847  cdlemefs32fvaN  35850  cdlemefs32fva1  35851  cdleme36m  35889  cdleme39a  35893  cdleme17d3  35924  cdleme50trn2  35979  cdlemg36  36142  cdlemj3  36251  cdlemkfid1N  36349  cdlemkid1  36350  cdlemk19ylem  36358  cdlemk19xlem  36370  dihlsscpre  36663  dihord4  36687  dihatlat  36763  mapdh9a  37219
  Copyright terms: Public domain W3C validator