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

Theorem simp-4l 743
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 735 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
21adantr 452 1  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  simp-5l  745  marypha1lem  7396  acndom2  7891  ttukeylem6  8350  fpwwe2lem12  8472  ramcl  13352  dfod2  15155  pgpfi  15194  ghmcyg  15460  neiptoptop  17150  cncnp  17298  subislly  17497  ptcnplem  17606  pthaus  17623  xkohaus  17638  kqreglem1  17726  cnextcn  18051  divstgplem  18103  trust  18212  utoptop  18217  restutopopn  18221  ustuqtop2  18225  ustuqtop3  18226  utop3cls  18234  utopreg  18235  isucn2  18262  met1stc  18504  metustsymOLD  18544  metustsym  18545  metustOLD  18550  metust  18551  metuel2  18562  xrge0tsms  18818  xmetdcn2  18821  nmoleub2lem2  19077  iscfil2  19172  iscfil3  19179  dvmptfsum  19812  dvlip2  19832  aannenlem1  20198  ulm2  20254  ulmuni  20261  mtestbdd  20274  efopn  20502  dchrptlem1  21001  pntpbnd  21235  pntibnd  21240  pthdepisspth  21527  cusconngra  21616  xrofsup  24079  xrge0tsmsd  24176  subofld  24198  sqsscirc1  24259  lmxrge0  24290  lmdvg  24291  esumfsup  24413  esumcvg  24429  btwnconn1lem13  25937  mblfinlem2  26144  mblfinlem3  26145  prdstotbnd  26393  rencldnfilem  26771  pellex  26788  pellfundex  26839  dvdsacongtr  26939  fnchoice  27567  climsuse  27601  usgra2pth  28041  ltrnid  30617
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