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

Theorem simpl3r 1013
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 986 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
21adantr 452 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  tfisi  4780  omopth2  6765  ltmul1a  9793  xmulasslem3  10799  xadddi2  10810  dvdsadd2b  12821  pockthg  13203  efgred  15309  ptbasin  17532  basqtop  17666  xrsmopn  18716  br4  25141  axpasch  25596  axeuclid  25618  btwnouttr2  25672  trisegint  25678  cgrxfr  25705  lineext  25726  btwnconn1lem13  25749  btwnconn1lem14  25750  btwnconn3  25753  brsegle  25758  brsegle2  25759  segleantisym  25765  outsideofeu  25781  lineunray  25797  lineelsb2  25798  qirropth  26664  mzpcong  26730  jm2.26  26766  aomclem6  26827  psgnunilem4  27091  cvrcmp  29400  atcvrj2b  29548  3dimlem3  29577  3dimlem3OLDN  29578  3dim3  29585  ps-1  29593  ps-2  29594  lplnnle2at  29657  2llnm3N  29685  4atlem0a  29709  4atlem3  29712  4atlem3a  29713  lnatexN  29895  paddasslem8  29943  paddasslem9  29944  paddasslem10  29945  paddasslem12  29947  paddasslem13  29948  lhpexle2lem  30125  lhpexle3  30128  lhpat3  30162  4atex  30192  trlval4  30304  cdleme16  30401  cdleme21  30453  cdleme21k  30454  cdleme27cl  30482  cdleme27N  30485  cdleme43fsv1snlem  30536  cdleme48fvg  30616  cdlemg8  30747  cdlemg15a  30771  cdlemg16z  30775  cdlemg24  30804  cdlemg38  30831  cdlemg40  30833  trlcone  30844  cdlemj2  30938  tendoid0  30941  tendoconid  30945  cdlemk34  31026  cdlemk38  31031  cdlemkid4  31050  cdlemk53  31073  tendospcanN  31140  dihvalcqpre  31352  dihmeetlem15N  31438
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator