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  8296  pwfseqlem5  8301  issubc3  13739  pgpfac1lem5  15330  clscon  17172  txlly  17346  txnlly  17347  itg2add  19130  ftc1a  19400  erdszelem7  23743  cvmlift2lem10  23858  ax5seglem6  24634  axcontlem9  24672  axcontlem10  24673  btwnouttr2  24717  btwnconn1lem13  24794  broutsideof2  24817  rltrooo  25518  limptlimpr2lem1  25677  limptlimpr2lem2  25678  lvsovso  25729  bosser  26270  icodiamlt  27008  mpaaeu  27458
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