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

Theorem simp-4l 758
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 750 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
21adantr 462 1  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  simp-5l  760  marypha1lem  7671  acndom2  8212  ttukeylem6  8671  fpwwe2lem12  8795  ramcl  14072  gsmsymgreqlem2  15915  dfod2  16044  pgpfi  16083  ghmcyg  16351  neiptoptop  18576  cncnp  18725  subislly  18926  ptcnplem  19035  pthaus  19052  xkohaus  19067  kqreglem1  19155  cnextcn  19480  divstgplem  19532  trust  19645  utoptop  19650  restutopopn  19654  ustuqtop2  19658  ustuqtop3  19659  utop3cls  19667  utopreg  19668  isucn2  19695  met1stc  19937  metustsymOLD  19977  metustsym  19978  metustOLD  19983  metust  19984  metuel2  19995  xrge0tsms  20252  xmetdcn2  20255  nmoleub2lem2  20512  iscfil2  20618  iscfil3  20625  dvmptfsum  21288  dvlip2  21308  aannenlem1  21678  ulm2  21734  ulmuni  21741  mtestbdd  21754  efopn  21987  dchrptlem1  22487  pntpbnd  22721  pntibnd  22726  legval  22890  f1otrg  22939  f1otrge  22940  pthdepisspth  23295  cusconngra  23384  xrofsup  25877  ressprs  25938  omndmul2  25998  isarchi3  26027  archirngz  26029  lmodslmd  26068  xrge0tsmsd  26105  suborng  26135  isarchiofld  26137  sqsscirc1  26191  lmxrge0  26235  lmdvg  26236  esumfsup  26372  esumcvg  26388  ddemeas  26505  btwnconn1lem13  27976  mblfinlem3  28271  mblfinlem4  28272  ftc1anclem7  28314  ftc1anc  28316  prdstotbnd  28534  rencldnfilem  29001  pellex  29018  pellfundex  29069  dvdsacongtr  29169  fnchoice  29593  climsuse  29624  reuccats1  30104  usgra2pth  30144  clwlkisclwwlklem2a4  30289  ltrnid  33349
  Copyright terms: Public domain W3C validator