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

Theorem simprl1 1003
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simprl1  |-  ( ( ta  /\  ( (
ph  /\  ps  /\  ch )  /\  th ) )  ->  ph )

Proof of Theorem simprl1
StepHypRef Expression
1 simpl1 961 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantl 454 1  |-  ( ( ta  /\  ( (
ph  /\  ps  /\  ch )  /\  th ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  pwfseqlem1  8535  pwfseqlem5  8540  issubc3  14048  pgpfac1lem5  15639  clscon  17495  txlly  17670  txnlly  17671  itg2add  19653  ftc1a  19923  erdszelem7  24885  cvmlift2lem10  25001  ax5seglem6  25875  axcontlem9  25913  axcontlem10  25914  btwnouttr2  25958  btwnconn1lem13  26035  broutsideof2  26058  icodiamlt  26885  mpaaeu  27334
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator