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

Theorem simpr2l 1056
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 1023 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
21adantl 466 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 185  df-an 371  df-3an 976
This theorem is referenced by:  oppccatid  14991  subccatid  15089  setccatid  15285  catccatid  15303  xpccatid  15331  gsmsymgreqlem1  16329  kerf1hrm  17266  nllyidm  19863  ax5seg  24113  segconeq  29635  ifscgr  29669  brofs2  29702  brifs2  29703  idinside  29709  btwnconn1lem8  29719  btwnconn1lem12  29723  segcon2  29730  segletr  29739  outsidele  29757  estrccatid  32484  lplnexllnN  35022  paddasslem9  35286  pmodlem2  35305  lhp2lt  35459  cdlemc3  35652  cdlemc4  35653  cdlemd1  35657  cdleme3b  35688  cdleme3c  35689  cdleme42ke  35945  cdlemg4c  36072
  Copyright terms: Public domain W3C validator