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

Theorem simp-4l 765
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 757 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
21adantr 465 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  767  marypha1lem  7704  acndom2  8245  ttukeylem6  8704  fpwwe2lem12  8829  ramcl  14111  gsmsymgreqlem2  15957  dfod2  16086  pgpfi  16125  ghmcyg  16393  neiptoptop  18757  cncnp  18906  subislly  19107  ptcnplem  19216  pthaus  19233  xkohaus  19248  kqreglem1  19336  cnextcn  19661  divstgplem  19713  trust  19826  utoptop  19831  restutopopn  19835  ustuqtop2  19839  ustuqtop3  19840  utop3cls  19848  utopreg  19849  isucn2  19876  met1stc  20118  metustsymOLD  20158  metustsym  20159  metustOLD  20164  metust  20165  metuel2  20176  xrge0tsms  20433  xmetdcn2  20436  nmoleub2lem2  20693  iscfil2  20799  iscfil3  20806  dvmptfsum  21469  dvlip2  21489  aannenlem1  21816  ulm2  21872  ulmuni  21879  mtestbdd  21892  efopn  22125  dchrptlem1  22625  pntpbnd  22859  pntibnd  22864  legval  23037  f1otrg  23139  f1otrge  23140  pthdepisspth  23495  cusconngra  23584  xrofsup  26077  ressprs  26138  omndmul2  26197  isarchi3  26226  archirngz  26228  lmodslmd  26242  xrge0tsmsd  26275  suborng  26305  isarchiofld  26307  sqsscirc1  26360  lmxrge0  26404  lmdvg  26405  esumfsup  26541  esumcvg  26557  ddemeas  26674  btwnconn1lem13  28152  mblfinlem3  28456  mblfinlem4  28457  ftc1anclem7  28499  ftc1anc  28501  prdstotbnd  28719  rencldnfilem  29185  pellex  29202  pellfundex  29253  dvdsacongtr  29353  fnchoice  29777  climsuse  29807  reuccats1  30287  usgra2pth  30327  clwlkisclwwlklem2a4  30472  cnstpmatmcllem  31070  pmatcollpw1dst  31116  pmattomply1mhmlem2  31144  ltrnid  33875
  Copyright terms: Public domain W3C validator