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  14650  subccatid  14748  setccatid  14944  catccatid  14962  xpccatid  14990  gsmsymgreqlem1  15924  nllyidm  19062  ax5seg  23129  kerf1hrm  26239  segconeq  27988  ifscgr  28022  brofs2  28055  brifs2  28056  idinside  28062  btwnconn1lem8  28072  btwnconn1lem12  28076  segcon2  28083  segletr  28092  outsidele  28110  lplnexllnN  32959  paddasslem9  33223  pmodlem2  33242  lhp2lt  33396  cdlemc3  33588  cdlemc4  33589  cdlemd1  33593  cdleme3b  33624  cdleme3c  33625  cdleme42ke  33880  cdlemg4c  34007
  Copyright terms: Public domain W3C validator