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 463 1  |-  ( ( ( ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  simp-7r  772  catass  15175  mhmmnd  16391  scmatscm  19182  cfilucfilOLD  21238  cfilucfil  21239  istrkgb  24050  istrkge  24052  tgbtwnconn1  24163  legso  24186  footex  24296  opphl  24326  f1otrg  24376  2sqmo  27871  pstmxmet  28111  signstfvneq0  28793  afsval  28815  mblfinlem3  30293  mblfinlem4  30294  limclner  31896  fourierdlem51  32179  iunconlem2  34136
  Copyright terms: Public domain W3C validator