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

Theorem simp1rl 1061
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 755 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant1 1017 1  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  f1imass  6158  smo11  7032  zsupss  11167  lsmcv  17567  lspsolvlem  17568  mat2pmatghm  18995  mat2pmatmul  18996  plyadd  22346  plymul  22347  coeeu  22354  aannenlem1  22455  logexprlim  23225  ax5seglem6  23910  ax5seg  23914  wsuclem  28955  btwnconn1lem2  29312  btwnconn1lem3  29313  btwnconn1lem4  29314  btwnconn1lem12  29322  pellex  30373  mullimc  31158  mullimcf  31165  limcperiod  31170  cncfshift  31212  cncfperiod  31217  lshpsmreu  33906  2llnmat  34320  lvolex3N  34334  lnjatN  34576  pclfinclN  34746  lhpat3  34842  cdlemd6  34999  cdlemfnid  35360  cdlemk19ylem  35726  dihlsscpre  36031  dih1dimb2  36038  dihglblem6  36137
  Copyright terms: Public domain W3C validator