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

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

Proof of Theorem simpl3r
StepHypRef Expression
1 simp3r 1037 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
21adantr 467 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  tfisi  6685  omopth2  7285  ltmul1a  10454  xmulasslem3  11572  xadddi2  11583  swrdsbslen  12804  swrdspsleq  12805  dvdsadd2b  14347  pockthg  14850  psgnunilem4  17138  efgred  17398  marrepeval  19588  submaeval  19607  mdetmul  19648  minmar1eval  19674  ptbasin  20592  basqtop  20726  xrsmopn  21830  axpasch  24971  axeuclid  24993  extwwlkfablem2  25806  br4  30398  btwnouttr2  30789  trisegint  30795  cgrxfr  30822  lineext  30843  btwnconn1lem13  30866  btwnconn1lem14  30867  btwnconn3  30870  brsegle  30875  brsegle2  30876  segleantisym  30882  outsideofeu  30898  lineunray  30914  lineelsb2  30915  cvrcmp  32849  atcvrj2b  32997  3dimlem3  33026  3dimlem3OLDN  33027  3dim3  33034  ps-1  33042  ps-2  33043  lplnnle2at  33106  2llnm3N  33134  4atlem0a  33158  4atlem3  33161  4atlem3a  33162  lnatexN  33344  paddasslem8  33392  paddasslem9  33393  paddasslem10  33394  paddasslem12  33396  paddasslem13  33397  lhpexle2lem  33574  lhpexle3  33577  lhpat3  33611  4atex  33641  trlval2  33729  trlval4  33754  cdleme16  33851  cdleme21  33904  cdleme21k  33905  cdleme27cl  33933  cdleme27N  33936  cdleme43fsv1snlem  33987  cdleme48fvg  34067  cdlemg8  34198  cdlemg15a  34222  cdlemg16z  34226  cdlemg24  34255  cdlemg38  34282  cdlemg40  34284  trlcone  34295  cdlemj2  34389  tendoid0  34392  tendoconid  34396  cdlemk34  34477  cdlemk38  34482  cdlemkid4  34501  cdlemk53  34524  tendospcanN  34591  dihvalcqpre  34803  dihmeetlem15N  34889  qirropth  35756  mzpcong  35822  jm2.26  35857  aomclem6  35917  islptre  37699  limccog  37700  limcleqr  37725  fourierdlem42  38012  fourierdlem42OLD  38013  elaa2  38099
  Copyright terms: Public domain W3C validator