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

Theorem simprl1 1041
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 999 . 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 973
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 975
This theorem is referenced by:  pwfseqlem1  9037  pwfseqlem5  9042  issubc3  15079  pgpfac1lem5  16944  clscon  19737  txlly  19964  txnlly  19965  itg2add  21993  ftc1a  22265  f1otrg  23947  ax5seglem6  24010  axcontlem9  24048  axcontlem10  24049  extwwlkfablem2  24852  erdszelem7  28392  cvmlift2lem10  28508  btwnouttr2  29525  btwnconn1lem13  29602  broutsideof2  29625  icodiamlt  30587  mpaaeu  30931
  Copyright terms: Public domain W3C validator