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

Theorem simpr2l 1016
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 983 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
21adantl 453 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  oppccatid  13904  subccatid  14002  setccatid  14198  catccatid  14216  xpccatid  14244  nllyidm  17509  kerf1hrm  24219  ax5seg  25785  segconeq  25852  ifscgr  25886  brofs2  25919  brifs2  25920  idinside  25926  btwnconn1lem8  25936  btwnconn1lem12  25940  segcon2  25947  segletr  25956  outsidele  25974  lplnexllnN  30050  paddasslem9  30314  pmodlem2  30333  lhp2lt  30487  cdlemc3  30679  cdlemc4  30680  cdlemd1  30684  cdleme3b  30715  cdleme3c  30716  cdleme42ke  30971  cdlemg4c  31098
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