MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1rl 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  5951  smo11  6564  zsupss  10499  lsmcv  16142  lspsolvlem  16143  plyadd  20005  plymul  20006  coeeu  20013  aannenlem1  20114  logexprlim  20878  ax5seglem6  25589  ax5seg  25593  btwnconn1lem2  25738  btwnconn1lem3  25739  btwnconn1lem4  25740  btwnconn1lem12  25748  pellex  26591  lshpsmreu  29226  2llnmat  29640  lvolex3N  29654  lnjatN  29896  pclfinclN  30066  lhpat3  30162  cdlemd6  30319  cdlemfnid  30680  cdlemk19ylem  31046  dihlsscpre  31351  dih1dimb2  31358  dihglblem6  31457
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