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

Theorem simp-5l 776
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 774 . 2  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ph )
21adantr 466 1  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  simp-6l  778  mhmmnd  16759  neiptopnei  20079  neitx  20553  ustex3sym  21163  restutop  21183  ustuqtop4  21190  utopreg  21198  xrge0tsms  21763  f1otrg  24747  usg2spot2nb  25638  xrge0tsmsd  28387  pstmxmet  28539  esumfsup  28730  esum2dlem  28752  esum2d  28753  omssubadd  28961  eulerpartlemgvv  29035  eldioph2  35316  limcrecl  37284  icccncfext  37340  ioodvbdlimc1lem2  37379  ioodvbdlimc2lem  37381  stoweidlem60  37493  fourierdlem77  37618  fourierdlem80  37621  fourierdlem103  37644  fourierdlem104  37645  etransclem35  37704
  Copyright terms: Public domain W3C validator