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

Theorem simp-4l 781
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 773 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
21adantr 471 1  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  simp-5l  783  marypha1lem  7934  acndom2  8472  ttukeylem6  8931  fpwwe2lem12  9053  reuccats1  12836  ramcl  14998  initoeu2lem1  15920  gsmsymgreqlem2  17083  dfod2  17226  pgpfi  17268  ghmcyg  17541  psgndif  19181  scmatmulcl  19554  cpmatmcllem  19753  neiptoptop  20158  cncnp  20307  subislly  20507  ptcnplem  20647  pthaus  20664  xkohaus  20679  kqreglem1  20767  cnextcn  21093  qustgplem  21146  trust  21255  utoptop  21260  restutopopn  21264  ustuqtop2  21268  ustuqtop3  21269  utop3cls  21277  utopreg  21278  isucn2  21305  met1stc  21547  metustsym  21581  metust  21584  metuel2  21591  xrge0tsms  21863  xmetdcn2  21866  nmoleub2lem2  22141  iscfil2  22247  iscfil3  22254  dvmptfsum  22939  dvlip2  22959  aannenlem1  23296  ulm2  23352  ulmuni  23359  mtestbdd  23372  efopn  23615  dchrptlem1  24204  pntpbnd  24438  pntibnd  24443  legval  24641  f1otrg  24913  f1otrge  24914  pthdepisspth  25316  usgra2adedgwlkonALT  25356  cusconngra  25416  clwlkisclwwlklem2a4  25524  xrofsup  28361  ressprs  28424  omndmul2  28482  isarchi3  28511  archirngz  28513  lmodslmd  28527  gsummpt2d  28551  xrge0tsmsd  28555  suborng  28585  isarchiofld  28587  sqsscirc1  28721  lmxrge0  28765  lmdvg  28766  esumrnmpt2  28896  esumfsup  28898  esumcvg  28914  esum2d  28921  ddemeas  29065  omssubadd  29134  omssubaddOLD  29138  btwnconn1lem13  30872  poimirlem29  31971  mblfinlem3  31981  mblfinlem4  31982  ftc1anclem7  32025  ftc1anc  32027  prdstotbnd  32128  ltrnid  33702  rencldnfilem  35665  pellex  35681  pellfundex  35736  dvdsacongtr  35836  fnchoice  37347  climsuse  37729  addlimc  37771  0ellimcdiv  37772  limclner  37774  icccncfext  37807  dvnprodlem3  37865  fourierdlem12  38038  fourierdlem34  38061  fourierdlem50  38077  fourierdlem80  38107  fourierdlem81  38108  fourierdlem87  38114  etransclem35  38191  sge0pr  38295  nbupgr  39514  pthdepissPth  39819  2pthon3v-av  39944  cusconngr  39984  usgra2pth  39993  uzlidlring  40254  2zlidl  40259
  Copyright terms: Public domain W3C validator