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

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

Proof of Theorem simp-4r
StepHypRef Expression
1 simpllr 735 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
21adantr 451 1  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  simp-5r  745  prdsval  13371  catcocl  13603  catass  13604  catpropd  13628  cidpropd  13629  monpropd  13656  subccocl  13735  funcco  13761  funcpropd  13790  fucpropd  13867  xpcpropd  13998  curf2ndf  14037  sqsscirc1  23307  lmxrge0  23390  esumcst  23451  wallispilem3  27919  injresinj  28215  pthdepisspth  28360
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