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

Theorem simp1rl 1022
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp1rl  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ph )

Proof of Theorem simp1rl
StepHypRef Expression
1 simprl 733 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant1 978 1  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  f1imass  6002  smo11  6618  zsupss  10557  lsmcv  16205  lspsolvlem  16206  plyadd  20128  plymul  20129  coeeu  20136  aannenlem1  20237  logexprlim  21001  wsuclem  25568  ax5seglem6  25865  ax5seg  25869  btwnconn1lem2  26014  btwnconn1lem3  26015  btwnconn1lem4  26016  btwnconn1lem12  26024  pellex  26889  lshpsmreu  29844  2llnmat  30258  lvolex3N  30272  lnjatN  30514  pclfinclN  30684  lhpat3  30780  cdlemd6  30937  cdlemfnid  31298  cdlemk19ylem  31664  dihlsscpre  31969  dih1dimb2  31976  dihglblem6  32075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator