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  7956  acndom2  8492  ttukeylem6  8951  fpwwe2lem12  9073  reuccats1  12839  ramcl  14986  initoeu2lem1  15908  gsmsymgreqlem2  17071  dfod2  17214  pgpfi  17256  ghmcyg  17529  psgndif  19168  scmatmulcl  19541  cpmatmcllem  19740  neiptoptop  20145  cncnp  20294  subislly  20494  ptcnplem  20634  pthaus  20651  xkohaus  20666  kqreglem1  20754  cnextcn  21080  qustgplem  21133  trust  21242  utoptop  21247  restutopopn  21251  ustuqtop2  21255  ustuqtop3  21256  utop3cls  21264  utopreg  21265  isucn2  21292  met1stc  21534  metustsym  21568  metust  21571  metuel2  21578  xrge0tsms  21850  xmetdcn2  21853  nmoleub2lem2  22128  iscfil2  22234  iscfil3  22241  dvmptfsum  22925  dvlip2  22945  aannenlem1  23282  ulm2  23338  ulmuni  23345  mtestbdd  23358  efopn  23601  dchrptlem1  24190  pntpbnd  24424  pntibnd  24429  legval  24627  f1otrg  24899  f1otrge  24900  pthdepisspth  25302  usgra2adedgwlkonALT  25342  cusconngra  25402  clwlkisclwwlklem2a4  25510  xrofsup  28359  ressprs  28423  omndmul2  28482  isarchi3  28511  archirngz  28513  lmodslmd  28527  gsummpt2d  28551  xrge0tsmsd  28556  suborng  28586  isarchiofld  28588  sqsscirc1  28722  lmxrge0  28766  lmdvg  28767  esumrnmpt2  28897  esumfsup  28899  esumcvg  28915  esum2d  28922  ddemeas  29067  omssubadd  29136  omssubaddOLD  29140  btwnconn1lem13  30871  poimirlem29  31933  mblfinlem3  31943  mblfinlem4  31944  ftc1anclem7  31987  ftc1anc  31989  prdstotbnd  32090  ltrnid  33669  rencldnfilem  35632  pellex  35649  pellfundex  35704  dvdsacongtr  35804  fnchoice  37323  climsuse  37627  addlimc  37669  0ellimcdiv  37670  limclner  37672  icccncfext  37705  dvnprodlem3  37763  fourierdlem12  37921  fourierdlem34  37944  fourierdlem50  37960  fourierdlem80  37990  fourierdlem81  37991  fourierdlem87  37997  etransclem35  38074  sge0pr  38144  usgra2pth  39288  uzlidlring  39549  2zlidl  39554
  Copyright terms: Public domain W3C validator