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

Theorem simpl3r 1013
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 986 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
21adantr 452 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  tfisi  4830  omopth2  6819  ltmul1a  9851  xmulasslem3  10857  xadddi2  10868  dvdsadd2b  12884  pockthg  13266  efgred  15372  ptbasin  17601  basqtop  17735  xrsmopn  18835  br4  25373  axpasch  25872  axeuclid  25894  btwnouttr2  25948  trisegint  25954  cgrxfr  25981  lineext  26002  btwnconn1lem13  26025  btwnconn1lem14  26026  btwnconn3  26029  brsegle  26034  brsegle2  26035  segleantisym  26041  outsideofeu  26057  lineunray  26073  lineelsb2  26074  qirropth  26962  mzpcong  27028  jm2.26  27064  aomclem6  27125  psgnunilem4  27388  cvrcmp  30018  atcvrj2b  30166  3dimlem3  30195  3dimlem3OLDN  30196  3dim3  30203  ps-1  30211  ps-2  30212  lplnnle2at  30275  2llnm3N  30303  4atlem0a  30327  4atlem3  30330  4atlem3a  30331  lnatexN  30513  paddasslem8  30561  paddasslem9  30562  paddasslem10  30563  paddasslem12  30565  paddasslem13  30566  lhpexle2lem  30743  lhpexle3  30746  lhpat3  30780  4atex  30810  trlval4  30922  cdleme16  31019  cdleme21  31071  cdleme21k  31072  cdleme27cl  31100  cdleme27N  31103  cdleme43fsv1snlem  31154  cdleme48fvg  31234  cdlemg8  31365  cdlemg15a  31389  cdlemg16z  31393  cdlemg24  31422  cdlemg38  31449  cdlemg40  31451  trlcone  31462  cdlemj2  31556  tendoid0  31559  tendoconid  31563  cdlemk34  31644  cdlemk38  31649  cdlemkid4  31668  cdlemk53  31691  tendospcanN  31758  dihvalcqpre  31970  dihmeetlem15N  32056
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator