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

Theorem simpr2l 1017
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 984 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
21adantl 454 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  oppccatid  13976  subccatid  14074  setccatid  14270  catccatid  14288  xpccatid  14316  nllyidm  17583  kerf1hrm  24293  ax5seg  25908  segconeq  25975  ifscgr  26009  brofs2  26042  brifs2  26043  idinside  26049  btwnconn1lem8  26059  btwnconn1lem12  26063  segcon2  26070  segletr  26079  outsidele  26097  lplnexllnN  30459  paddasslem9  30723  pmodlem2  30742  lhp2lt  30896  cdlemc3  31088  cdlemc4  31089  cdlemd1  31093  cdleme3b  31124  cdleme3c  31125  cdleme42ke  31380  cdlemg4c  31507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator