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

Theorem simp1rl 1053
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 1009 1  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  f1imass  6089  smo11  6938  zsupss  11058  lsmcv  17348  lspsolvlem  17349  plyadd  21821  plymul  21822  coeeu  21829  aannenlem1  21930  logexprlim  22700  ax5seglem6  23352  ax5seg  23356  wsuclem  27926  btwnconn1lem2  28283  btwnconn1lem3  28284  btwnconn1lem4  28285  btwnconn1lem12  28293  pellex  29344  mat2pmatghm  31239  mat2pmatmul  31240  lshpsmreu  33112  2llnmat  33526  lvolex3N  33540  lnjatN  33782  pclfinclN  33952  lhpat3  34048  cdlemd6  34205  cdlemfnid  34566  cdlemk19ylem  34932  dihlsscpre  35237  dih1dimb2  35244  dihglblem6  35343
  Copyright terms: Public domain W3C validator