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

Theorem simpr2l 1014
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpr2l  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ph )

Proof of Theorem simpr2l
StepHypRef Expression
1 simp2l 981 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
21adantl 452 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  oppccatid  13715  subccatid  13813  setccatid  14009  catccatid  14027  xpccatid  14055  nllyidm  17315  kerf1hrm  23428  ax5seg  25125  segconeq  25192  ifscgr  25226  brofs2  25259  brifs2  25260  idinside  25266  btwnconn1lem8  25276  btwnconn1lem12  25280  segcon2  25287  segletr  25296  outsidele  25314  lplnexllnN  29805  paddasslem9  30069  pmodlem2  30088  lhp2lt  30242  cdlemc3  30434  cdlemc4  30435  cdlemd1  30439  cdleme3b  30470  cdleme3c  30471  cdleme42ke  30726  cdlemg4c  30853
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