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  13622  subccatid  13720  setccatid  13916  catccatid  13934  xpccatid  13962  nllyidm  17215  ax5seg  24566  segconeq  24633  ifscgr  24667  brofs2  24700  brifs2  24701  idinside  24707  btwnconn1lem8  24717  btwnconn1lem12  24721  segcon2  24728  segletr  24737  outsidele  24755  icmpmon  25816  domsubc  25852  clscnc  26010  lplnexllnN  29753  paddasslem9  30017  pmodlem2  30036  lhp2lt  30190  cdlemc3  30382  cdlemc4  30383  cdlemd1  30387  cdleme3b  30418  cdleme3c  30419  cdleme42ke  30674  cdlemg4c  30801
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