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  7893  acndom2  8435  ttukeylem6  8894  fpwwe2lem12  9019  reuccats1  12669  ramcl  14406  gsmsymgreqlem2  16261  dfod2  16392  pgpfi  16431  ghmcyg  16701  scmatmulcl  18815  cpmatmcllem  19014  neiptoptop  19426  cncnp  19575  subislly  19776  ptcnplem  19885  pthaus  19902  xkohaus  19917  kqreglem1  20005  cnextcn  20330  divstgplem  20382  trust  20495  utoptop  20500  restutopopn  20504  ustuqtop2  20508  ustuqtop3  20509  utop3cls  20517  utopreg  20518  isucn2  20545  met1stc  20787  metustsymOLD  20827  metustsym  20828  metustOLD  20833  metust  20834  metuel2  20845  xrge0tsms  21102  xmetdcn2  21105  nmoleub2lem2  21362  iscfil2  21468  iscfil3  21475  dvmptfsum  22139  dvlip2  22159  aannenlem1  22486  ulm2  22542  ulmuni  22549  mtestbdd  22562  efopn  22795  dchrptlem1  23295  pntpbnd  23529  pntibnd  23534  legval  23726  f1otrg  23878  f1otrge  23879  pthdepisspth  24280  usgra2adedgwlkonALT  24320  cusconngra  24380  clwlkisclwwlklem2a4  24488  xrofsup  27278  ressprs  27333  omndmul2  27392  isarchi3  27421  archirngz  27423  lmodslmd  27437  xrge0tsmsd  27466  suborng  27496  isarchiofld  27498  sqsscirc1  27554  lmxrge0  27598  lmdvg  27599  esumfsup  27744  esumcvg  27760  ddemeas  27876  btwnconn1lem13  29354  mblfinlem3  29658  mblfinlem4  29659  ftc1anclem7  29701  ftc1anc  29703  prdstotbnd  29921  rencldnfilem  30386  pellex  30403  pellfundex  30454  dvdsacongtr  30554  fnchoice  31010  climsuse  31178  addlimc  31218  0ellimcdiv  31219  limclner  31221  icccncfext  31254  fourierdlem12  31447  fourierdlem34  31469  fourierdlem50  31485  fourierdlem80  31515  fourierdlem81  31516  fourierdlem87  31522  usgra2pth  31849  ltrnid  34949
  Copyright terms: Public domain W3C validator