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

Theorem simpr2l 1053
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 1020 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
21adantl 464 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  oppccatid  15207  subccatid  15334  setccatid  15562  catccatid  15580  estrccatid  15600  xpccatid  15656  gsmsymgreqlem1  16654  kerf1hrm  17587  nllyidm  20156  ax5seg  24443  segconeq  29888  ifscgr  29922  brofs2  29955  brifs2  29956  idinside  29962  btwnconn1lem8  29972  btwnconn1lem12  29976  segcon2  29983  segletr  29992  outsidele  30010  lplnexllnN  35685  paddasslem9  35949  pmodlem2  35968  lhp2lt  36122  cdlemc3  36315  cdlemc4  36316  cdlemd1  36320  cdleme3b  36351  cdleme3c  36352  cdleme42ke  36608  cdlemg4c  36735
  Copyright terms: Public domain W3C validator