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

Theorem simprl1 1033
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 991 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantl 466 1  |-  ( ( ta  /\  ( (
ph  /\  ps  /\  ch )  /\  th ) )  ->  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:  pwfseqlem1  8825  pwfseqlem5  8830  issubc3  14759  pgpfac1lem5  16580  clscon  19034  txlly  19209  txnlly  19210  itg2add  21237  ftc1a  21509  f1otrg  23117  ax5seglem6  23180  axcontlem9  23218  axcontlem10  23219  erdszelem7  27085  cvmlift2lem10  27201  btwnouttr2  28053  btwnconn1lem13  28130  broutsideof2  28153  icodiamlt  29161  mpaaeu  29507  extwwlkfablem2  30671
  Copyright terms: Public domain W3C validator