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

Theorem simp3rl 1028
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 732 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant3 978 1  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  omeu  6585  hashbclem  11392  tsmsxp  17839  tgqioo  18308  ovolunlem2  18859  plyadd  19601  plymul  19602  coeeu  19609  gxmul  20947  cvmlift2lem10  23845  btwnconn1lem1  24712  btwnconn1lem2  24713  btwnconn1lem12  24723  injsurinj  25160  jm2.27  27112  lplnexllnN  29826  2llnjN  29829  4atlem12b  29873  lplncvrlvol2  29877  lncmp  30045  cdlema2N  30054  cdlemc2  30454  cdleme11a  30522  cdleme22eALTN  30607  cdleme24  30614  cdleme27a  30629  cdleme27N  30631  cdleme28  30635  cdlemefs29bpre0N  30678  cdlemefs29bpre1N  30679  cdlemefs29cpre1N  30680  cdlemefs29clN  30681  cdlemefs32fvaN  30684  cdlemefs32fva1  30685  cdleme36m  30723  cdleme39a  30727  cdleme17d3  30758  cdleme50trn2  30813  cdlemg36  30976  cdlemj3  31085  cdlemkfid1N  31183  cdlemkid1  31184  cdlemk19ylem  31192  cdlemk19xlem  31204  dihlsscpre  31497  dihord4  31521  dihatlat  31597  mapdh9a  32053
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