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

Theorem simp-4l 744
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 736 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
21adantr 453 1  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  simp-5l  746  marypha1lem  7440  acndom2  7937  ttukeylem6  8396  fpwwe2lem12  8518  ramcl  13399  dfod2  15202  pgpfi  15241  ghmcyg  15507  neiptoptop  17197  cncnp  17346  subislly  17546  ptcnplem  17655  pthaus  17672  xkohaus  17687  kqreglem1  17775  cnextcn  18100  divstgplem  18152  trust  18261  utoptop  18266  restutopopn  18270  ustuqtop2  18274  ustuqtop3  18275  utop3cls  18283  utopreg  18284  isucn2  18311  met1stc  18553  metustsymOLD  18593  metustsym  18594  metustOLD  18599  metust  18600  metuel2  18611  xrge0tsms  18867  xmetdcn2  18870  nmoleub2lem2  19126  iscfil2  19221  iscfil3  19228  dvmptfsum  19861  dvlip2  19881  aannenlem1  20247  ulm2  20303  ulmuni  20310  mtestbdd  20323  efopn  20551  dchrptlem1  21050  pntpbnd  21284  pntibnd  21289  pthdepisspth  21576  cusconngra  21665  xrofsup  24128  xrge0tsmsd  24225  subofld  24247  sqsscirc1  24308  lmxrge0  24339  lmdvg  24340  esumfsup  24462  esumcvg  24478  btwnconn1lem13  26035  mblfinlem3  26247  mblfinlem4  26248  ftc1anclem7  26288  ftc1anc  26290  prdstotbnd  26505  rencldnfilem  26883  pellex  26900  pellfundex  26951  dvdsacongtr  27051  fnchoice  27678  climsuse  27712  usgra2pth  28337  ltrnid  30994
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 179  df-an 362
  Copyright terms: Public domain W3C validator