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  4649  omopth2  6582  ltmul1a  9605  xmulasslem3  10606  xadddi2  10617  dvdsadd2b  12571  pockthg  12953  efgred  15057  ptbasin  17272  basqtop  17402  xrsmopn  18318  br4  24115  axpasch  24569  axeuclid  24591  btwnouttr2  24645  trisegint  24651  cgrxfr  24678  lineext  24699  btwnconn1lem13  24722  btwnconn1lem14  24723  btwnconn3  24726  brsegle  24731  brsegle2  24732  segleantisym  24738  outsideofeu  24754  lineunray  24770  lineelsb2  24771  iccss3  25134  cmprltr  25410  mulmulvec  25687  distmlva  25688  idmon  25817  isconcl5ab  26102  qirropth  26993  mzpcong  27059  jm2.26  27095  aomclem6  27156  psgnunilem4  27420  cvrcmp  29473  atcvrj2b  29621  3dimlem3  29650  3dimlem3OLDN  29651  3dim3  29658  ps-1  29666  ps-2  29667  lplnnle2at  29730  2llnm3N  29758  4atlem0a  29782  4atlem3  29785  4atlem3a  29786  lnatexN  29968  paddasslem8  30016  paddasslem9  30017  paddasslem10  30018  paddasslem12  30020  paddasslem13  30021  lhpexle2lem  30198  lhpexle3  30201  lhpat3  30235  4atex  30265  trlval4  30377  cdleme16  30474  cdleme21  30526  cdleme21k  30527  cdleme27cl  30555  cdleme27N  30558  cdleme43fsv1snlem  30609  cdleme48fvg  30689  cdlemg8  30820  cdlemg15a  30844  cdlemg16z  30848  cdlemg24  30877  cdlemg38  30904  cdlemg40  30906  trlcone  30917  cdlemj2  31011  tendoid0  31014  tendoconid  31018  cdlemk34  31099  cdlemk38  31104  cdlemkid4  31123  cdlemk53  31146  tendospcanN  31213  dihvalcqpre  31425  dihmeetlem15N  31511
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