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

Theorem simpl3r 1011
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 984 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
21adantr 451 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  tfisi  4665  omopth2  6598  ltmul1a  9621  xmulasslem3  10622  xadddi2  10633  dvdsadd2b  12587  pockthg  12969  efgred  15073  ptbasin  17288  basqtop  17418  xrsmopn  18334  br4  24186  axpasch  24641  axeuclid  24663  btwnouttr2  24717  trisegint  24723  cgrxfr  24750  lineext  24771  btwnconn1lem13  24794  btwnconn1lem14  24795  btwnconn3  24798  brsegle  24803  brsegle2  24804  segleantisym  24810  outsideofeu  24826  lineunray  24842  lineelsb2  24843  iccss3  25237  cmprltr  25513  mulmulvec  25790  distmlva  25791  idmon  25920  isconcl5ab  26205  qirropth  27096  mzpcong  27162  jm2.26  27198  aomclem6  27259  psgnunilem4  27523  cvrcmp  30095  atcvrj2b  30243  3dimlem3  30272  3dimlem3OLDN  30273  3dim3  30280  ps-1  30288  ps-2  30289  lplnnle2at  30352  2llnm3N  30380  4atlem0a  30404  4atlem3  30407  4atlem3a  30408  lnatexN  30590  paddasslem8  30638  paddasslem9  30639  paddasslem10  30640  paddasslem12  30642  paddasslem13  30643  lhpexle2lem  30820  lhpexle3  30823  lhpat3  30857  4atex  30887  trlval4  30999  cdleme16  31096  cdleme21  31148  cdleme21k  31149  cdleme27cl  31177  cdleme27N  31180  cdleme43fsv1snlem  31231  cdleme48fvg  31311  cdlemg8  31442  cdlemg15a  31466  cdlemg16z  31470  cdlemg24  31499  cdlemg38  31526  cdlemg40  31528  trlcone  31539  cdlemj2  31633  tendoid0  31636  tendoconid  31640  cdlemk34  31721  cdlemk38  31726  cdlemkid4  31745  cdlemk53  31768  tendospcanN  31835  dihvalcqpre  32047  dihmeetlem15N  32133
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator