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

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

Proof of Theorem simp-4l
StepHypRef Expression
1 simplll 734 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
21adantr 451 1  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  simp-5l  744  ulmuni  19869  mtestbdd  19882  xrofsup  23324  neiptoptop  23444  sqsscirc1  23462  lmxrge0  23493  lmdvg  23494  cnextcn  23504  trust  23533  utoptop  23538  restutopopn  23542  ustuqtop2  23546  ustuqtop3  23547  metustsym  23599  esumfsup  23726  esumcvg  23742  climsuse  27057  wallispilem3  27139  pthdepisspth  27699  cusconngra  27783
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 177  df-an 360
  Copyright terms: Public domain W3C validator