MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-6r Structured version   Unicode version

Theorem simp-6r 770
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-6r  |-  ( ( ( ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )

Proof of Theorem simp-6r
StepHypRef Expression
1 simp-5r 768 . 2  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
21adantr 465 1  |-  ( ( ( ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  simp-7r  772  catass  14645  cfilucfilOLD  20166  cfilucfil  20167  istrkgb  22940  istrkge  22942  tgbtwnconn1  23029  footex  23131  f1otrg  23139  pstmxmet  26346  signstfvneq0  26995  afsval  27017  mblfinlem3  28456  mblfinlem4  28457  iunconlem2  31767
  Copyright terms: Public domain W3C validator