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

Theorem simp-5l 745
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 743 . 2  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ph )
21adantr 452 1  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  simp-6l  747  neiptopnei  17188  neitx  17631  ustex3sym  18239  restutop  18259  ustuqtop4  18266  utopreg  18274  xrge0tsms  18857  xrge0tsmsd  24215  subofld  24237  pstmxmet  24284  esumfsup  24452  eldioph2  26811  stoweidlem60  27776  usg2spot2nb  28391
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator