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

Theorem simp-4r 744
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 736 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
21adantr 452 1  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  simp-5r  746  injresinj  11192  prdsval  13670  catcocl  13902  catass  13903  catpropd  13927  cidpropd  13928  monpropd  13955  subccocl  14034  funcco  14060  funcpropd  14089  fucpropd  14166  xpcpropd  14297  curf2ndf  14336  drsdirfi  14387  dfod2  15192  neitr  17236  1stcrest  17508  neitx  17631  tgqtop  17736  ptcmplem3  18077  trust  18251  utoptop  18256  restutopopn  18260  ustuqtop2  18264  ustuqtop4  18266  utop3cls  18273  isucn2  18301  met1stc  18543  prdsxmslem2  18551  metustexhalfOLD  18585  metustexhalf  18586  cfilucfilOLD  18591  cfilucfil  18592  metucnOLD  18610  metucn  18611  aannenlem1  20237  ulmuni  20300  pntpbnd  21274  pntlem3  21295  pthdepisspth  21566  subofld  24237  pstmxmet  24284  sqsscirc1  24298  lmxrge0  24329  esumcst  24447  esumfsup  24452  lgamucov  24814  axcontlem2  25896  mblfinlem2  26235  itg2addnclem  26246  nn0prpwlem  26316  sstotbnd2  26474  prdstotbnd  26494  diophren  26865  rencldnfilem  26872  pellex  26889  pell1234qrdich  26915  pell1qrgap  26928  pellfundex  26940  iunconlem2  28984  lcfl8  32237
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