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

Theorem simpl3r 1061
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 1034 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
21adantr 466 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  tfisi  6699  omopth2  7293  ltmul1a  10453  xmulasslem3  11572  xadddi2  11583  swrdsbslen  12789  swrdspsleq  12790  dvdsadd2b  14325  pockthg  14813  psgnunilem4  17093  efgred  17337  marrepeval  19523  submaeval  19542  mdetmul  19583  minmar1eval  19609  ptbasin  20527  basqtop  20661  xrsmopn  21745  axpasch  24825  axeuclid  24847  extwwlkfablem2  25659  br4  30193  btwnouttr2  30582  trisegint  30588  cgrxfr  30615  lineext  30636  btwnconn1lem13  30659  btwnconn1lem14  30660  btwnconn3  30663  brsegle  30668  brsegle2  30669  segleantisym  30675  outsideofeu  30691  lineunray  30707  lineelsb2  30708  cvrcmp  32569  atcvrj2b  32717  3dimlem3  32746  3dimlem3OLDN  32747  3dim3  32754  ps-1  32762  ps-2  32763  lplnnle2at  32826  2llnm3N  32854  4atlem0a  32878  4atlem3  32881  4atlem3a  32882  lnatexN  33064  paddasslem8  33112  paddasslem9  33113  paddasslem10  33114  paddasslem12  33116  paddasslem13  33117  lhpexle2lem  33294  lhpexle3  33297  lhpat3  33331  4atex  33361  trlval2  33449  trlval4  33474  cdleme16  33571  cdleme21  33624  cdleme21k  33625  cdleme27cl  33653  cdleme27N  33656  cdleme43fsv1snlem  33707  cdleme48fvg  33787  cdlemg8  33918  cdlemg15a  33942  cdlemg16z  33946  cdlemg24  33975  cdlemg38  34002  cdlemg40  34004  trlcone  34015  cdlemj2  34109  tendoid0  34112  tendoconid  34116  cdlemk34  34197  cdlemk38  34202  cdlemkid4  34221  cdlemk53  34244  tendospcanN  34311  dihvalcqpre  34523  dihmeetlem15N  34609  qirropth  35477  mzpcong  35543  jm2.26  35578  aomclem6  35638  islptre  37286  limccog  37287  limcleqr  37312  fourierdlem42  37595  elaa2  37681
  Copyright terms: Public domain W3C validator