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

Theorem simp-4l 774
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 766 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
21adantr 466 1  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  simp-5l  776  marypha1lem  7953  acndom2  8483  ttukeylem6  8942  fpwwe2lem12  9065  reuccats1  12822  ramcl  14950  initoeu2lem1  15860  gsmsymgreqlem2  17023  dfod2  17153  pgpfi  17192  ghmcyg  17465  psgndif  19101  scmatmulcl  19474  cpmatmcllem  19673  neiptoptop  20078  cncnp  20227  subislly  20427  ptcnplem  20567  pthaus  20584  xkohaus  20599  kqreglem1  20687  cnextcn  21013  qustgplem  21066  trust  21175  utoptop  21180  restutopopn  21184  ustuqtop2  21188  ustuqtop3  21189  utop3cls  21197  utopreg  21198  isucn2  21225  met1stc  21467  metustsym  21501  metust  21504  metuel2  21511  xrge0tsms  21763  xmetdcn2  21766  nmoleub2lem2  22023  iscfil2  22129  iscfil3  22136  dvmptfsum  22804  dvlip2  22824  aannenlem1  23149  ulm2  23205  ulmuni  23212  mtestbdd  23225  efopn  23468  dchrptlem1  24055  pntpbnd  24289  pntibnd  24294  legval  24489  f1otrg  24747  f1otrge  24748  pthdepisspth  25149  usgra2adedgwlkonALT  25189  cusconngra  25249  clwlkisclwwlklem2a4  25357  xrofsup  28189  ressprs  28254  omndmul2  28313  isarchi3  28342  archirngz  28344  lmodslmd  28358  gsummpt2d  28382  xrge0tsmsd  28387  suborng  28417  isarchiofld  28419  sqsscirc1  28553  lmxrge0  28597  lmdvg  28598  esumrnmpt2  28728  esumfsup  28730  esumcvg  28746  esum2d  28753  ddemeas  28898  omssubadd  28961  btwnconn1lem13  30651  poimirlem29  31672  mblfinlem3  31682  mblfinlem4  31683  ftc1anclem7  31726  ftc1anc  31728  prdstotbnd  31829  ltrnid  33408  rencldnfilem  35371  pellex  35388  pellfundex  35439  dvdsacongtr  35539  fnchoice  36989  climsuse  37258  addlimc  37300  0ellimcdiv  37301  limclner  37303  icccncfext  37336  dvnprodlem3  37391  fourierdlem12  37549  fourierdlem34  37571  fourierdlem50  37587  fourierdlem80  37617  fourierdlem81  37618  fourierdlem87  37624  etransclem35  37700  sge0pr  37769  usgra2pth  38423  uzlidlring  38686  2zlidl  38691
  Copyright terms: Public domain W3C validator