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  5804  smo11  6397  zsupss  10323  lsmcv  15910  lspsolvlem  15911  plyadd  19615  plymul  19616  coeeu  19623  aannenlem1  19724  logexprlim  20480  ax5seglem6  24634  ax5seg  24638  btwnconn1lem2  24783  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem12  24793  pellex  27023  lshpsmreu  29921  2llnmat  30335  lvolex3N  30349  lnjatN  30591  pclfinclN  30761  lhpat3  30857  cdlemd6  31014  cdlemfnid  31375  cdlemk19ylem  31741  dihlsscpre  32046  dih1dimb2  32053  dihglblem6  32152
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