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  19427  neitx  19871  ustex3sym  20483  restutop  20503  ustuqtop4  20510  utopreg  20518  xrge0tsms  21102  f1otrg  23878  usg2spot2nb  24770  xrge0tsmsd  27466  pstmxmet  27540  esumfsup  27744  eulerpartlemgvv  27983  eldioph2  30327  limcrecl  31199  icccncfext  31254  ioodvbdlimc1lem2  31290  ioodvbdlimc2lem  31292  stoweidlem60  31388  fourierdlem77  31512  fourierdlem80  31515  fourierdlem103  31538  fourierdlem104  31539
  Copyright terms: Public domain W3C validator