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

Theorem simpl3r 1052
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 1025 . 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 973
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 975
This theorem is referenced by:  tfisi  6677  omopth2  7233  ltmul1a  10391  xmulasslem3  11478  xadddi2  11489  dvdsadd2b  13887  pockthg  14283  psgnunilem4  16328  efgred  16572  marrepeval  18860  submaeval  18879  mdetmul  18920  minmar1eval  18946  ptbasin  19841  basqtop  19975  xrsmopn  21080  axpasch  23948  axeuclid  23970  extwwlkfablem2  24783  br4  28792  btwnouttr2  29277  trisegint  29283  cgrxfr  29310  lineext  29331  btwnconn1lem13  29354  btwnconn1lem14  29355  btwnconn3  29358  brsegle  29363  brsegle2  29364  segleantisym  29370  outsideofeu  29386  lineunray  29402  lineelsb2  29403  qirropth  30476  mzpcong  30542  jm2.26  30576  aomclem6  30637  islptre  31189  limccog  31190  limcleqr  31214  fourierdlem42  31477  cvrcmp  34098  atcvrj2b  34246  3dimlem3  34275  3dimlem3OLDN  34276  3dim3  34283  ps-1  34291  ps-2  34292  lplnnle2at  34355  2llnm3N  34383  4atlem0a  34407  4atlem3  34410  4atlem3a  34411  lnatexN  34593  paddasslem8  34641  paddasslem9  34642  paddasslem10  34643  paddasslem12  34645  paddasslem13  34646  lhpexle2lem  34823  lhpexle3  34826  lhpat3  34860  4atex  34890  trlval2  34977  trlval4  35002  cdleme16  35099  cdleme21  35151  cdleme21k  35152  cdleme27cl  35180  cdleme27N  35183  cdleme43fsv1snlem  35234  cdleme48fvg  35314  cdlemg8  35445  cdlemg15a  35469  cdlemg16z  35473  cdlemg24  35502  cdlemg38  35529  cdlemg40  35531  trlcone  35542  cdlemj2  35636  tendoid0  35639  tendoconid  35643  cdlemk34  35724  cdlemk38  35729  cdlemkid4  35748  cdlemk53  35771  tendospcanN  35838  dihvalcqpre  36050  dihmeetlem15N  36136
  Copyright terms: Public domain W3C validator