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

Theorem simpl3r 1044
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 1017 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
21adantr 465 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  tfisi  6467  omopth2  7021  ltmul1a  10176  xmulasslem3  11247  xadddi2  11258  dvdsadd2b  13573  pockthg  13965  psgnunilem4  16001  efgred  16243  marrepeval  18372  submaeval  18391  mdetmul  18427  minmar1eval  18453  ptbasin  19148  basqtop  19282  xrsmopn  20387  axpasch  23185  axeuclid  23207  br4  27566  btwnouttr2  28051  trisegint  28057  cgrxfr  28084  lineext  28105  btwnconn1lem13  28128  btwnconn1lem14  28129  btwnconn3  28132  brsegle  28137  brsegle2  28138  segleantisym  28144  outsideofeu  28160  lineunray  28176  lineelsb2  28177  qirropth  29246  mzpcong  29312  jm2.26  29348  aomclem6  29409  extwwlkfablem2  30668  cvrcmp  32925  atcvrj2b  33073  3dimlem3  33102  3dimlem3OLDN  33103  3dim3  33110  ps-1  33118  ps-2  33119  lplnnle2at  33182  2llnm3N  33210  4atlem0a  33234  4atlem3  33237  4atlem3a  33238  lnatexN  33420  paddasslem8  33468  paddasslem9  33469  paddasslem10  33470  paddasslem12  33472  paddasslem13  33473  lhpexle2lem  33650  lhpexle3  33653  lhpat3  33687  4atex  33717  trlval2  33804  trlval4  33829  cdleme16  33926  cdleme21  33978  cdleme21k  33979  cdleme27cl  34007  cdleme27N  34010  cdleme43fsv1snlem  34061  cdleme48fvg  34141  cdlemg8  34272  cdlemg15a  34296  cdlemg16z  34300  cdlemg24  34329  cdlemg38  34356  cdlemg40  34358  trlcone  34369  cdlemj2  34463  tendoid0  34466  tendoconid  34470  cdlemk34  34551  cdlemk38  34556  cdlemkid4  34575  cdlemk53  34598  tendospcanN  34665  dihvalcqpre  34877  dihmeetlem15N  34963
  Copyright terms: Public domain W3C validator