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

Theorem simp1rl 1059
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 754 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant1 1015 1  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  f1imass  6147  smo11  7027  zsupss  11172  lsmcv  17985  lspsolvlem  17986  mat2pmatghm  19401  mat2pmatmul  19402  plyadd  22783  plymul  22784  coeeu  22791  aannenlem1  22893  logexprlim  23701  ax5seglem6  24442  ax5seg  24446  wsuclem  29624  btwnconn1lem2  29969  btwnconn1lem3  29970  btwnconn1lem4  29971  btwnconn1lem12  29979  pellex  31013  mullimc  31864  mullimcf  31871  limcperiod  31876  cncfshift  31918  cncfperiod  31923  lshpsmreu  35250  2llnmat  35664  lvolex3N  35678  lnjatN  35920  pclfinclN  36090  lhpat3  36186  cdlemd6  36344  cdlemfnid  36706  cdlemk19ylem  37072  dihlsscpre  37377  dih1dimb2  37384  dihglblem6  37483
  Copyright terms: Public domain W3C validator