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

Theorem simprl1 1000
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 958 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantl 452 1  |-  ( ( ta  /\  ( (
ph  /\  ps  /\  ch )  /\  th ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pwfseqlem1  8280  pwfseqlem5  8285  issubc3  13723  pgpfac1lem5  15314  clscon  17156  txlly  17330  txnlly  17331  itg2add  19114  ftc1a  19384  erdszelem7  23728  cvmlift2lem10  23843  ax5seglem6  24562  axcontlem9  24600  axcontlem10  24601  btwnouttr2  24645  btwnconn1lem13  24722  broutsideof2  24745  rltrooo  25415  limptlimpr2lem1  25574  limptlimpr2lem2  25575  lvsovso  25626  bosser  26167  icodiamlt  26905  mpaaeu  27355
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