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

Theorem simprl1 1050
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 1008 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantl 467 1  |-  ( ( ta  /\  ( (
ph  /\  ps  /\  ch )  /\  th ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  pwfseqlem1  9082  pwfseqlem5  9087  issubc3  15705  pgpfac1lem5  17647  clscon  20376  txlly  20582  txnlly  20583  itg2add  22594  ftc1a  22866  f1otrg  24747  ax5seglem6  24810  axcontlem9  24848  axcontlem10  24849  extwwlkfablem2  25651  locfinref  28507  erdszelem7  29708  cvmlift2lem10  29823  btwnouttr2  30574  btwnconn1lem13  30651  broutsideof2  30674  icodiamlt  35374  mpaaeu  35715  digexp  39188
  Copyright terms: Public domain W3C validator