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

Theorem simp1rl 1020
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 732 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  f1imass  5788  smo11  6381  zsupss  10307  lsmcv  15894  lspsolvlem  15895  plyadd  19599  plymul  19600  coeeu  19607  aannenlem1  19708  logexprlim  20464  ax5seglem6  24562  ax5seg  24566  btwnconn1lem2  24711  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem12  24721  pellex  26920  lshpsmreu  29299  2llnmat  29713  lvolex3N  29727  lnjatN  29969  pclfinclN  30139  lhpat3  30235  cdlemd6  30392  cdlemfnid  30753  cdlemk19ylem  31119  dihlsscpre  31424  dih1dimb2  31431  dihglblem6  31530
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator