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

Theorem simpr2l 1047
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 1014 . 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 965
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 967
This theorem is referenced by:  oppccatid  14760  subccatid  14858  setccatid  15054  catccatid  15072  xpccatid  15100  gsmsymgreqlem1  16037  kerf1hrm  16937  nllyidm  19209  ax5seg  23319  segconeq  28175  ifscgr  28209  brofs2  28242  brifs2  28243  idinside  28249  btwnconn1lem8  28259  btwnconn1lem12  28263  segcon2  28270  segletr  28279  outsidele  28297  lplnexllnN  33514  paddasslem9  33778  pmodlem2  33797  lhp2lt  33951  cdlemc3  34143  cdlemc4  34144  cdlemd1  34148  cdleme3b  34179  cdleme3c  34180  cdleme42ke  34435  cdlemg4c  34562
  Copyright terms: Public domain W3C validator