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

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

Proof of Theorem simp-5l
StepHypRef Expression
1 simp-4l 765 . 2  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ph )
21adantr 465 1  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ph )
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-6l  769  neiptopnei  18751  neitx  19195  ustex3sym  19807  restutop  19827  ustuqtop4  19834  utopreg  19842  xrge0tsms  20426  f1otrg  23132  xrge0tsmsd  26268  pstmxmet  26339  esumfsup  26534  eulerpartlemgvv  26774  eldioph2  29119  stoweidlem60  29874  usg2spot2nb  30677
  Copyright terms: Public domain W3C validator