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

Theorem simp-4l 801
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-4l (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simp-4l
StepHypRef Expression
1 simplll 793 . 2 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
21adantr 479 1 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  simp-5l  803  marypha1lem  8194  acndom2  8732  ttukeylem6  9191  fpwwe2lem12  9314  reuccats1  13273  dfgcd2  15042  ramcl  15512  initoeu2lem1  16428  gsmsymgreqlem2  17615  dfod2  17745  pgpfi  17784  ghmcyg  18061  psgndif  19707  scmatmulcl  20080  cpmatmcllem  20279  neiptoptop  20682  cncnp  20831  subislly  21031  ptcnplem  21171  pthaus  21188  xkohaus  21203  kqreglem1  21291  cnextcn  21618  qustgplem  21671  trust  21780  utoptop  21785  restutopopn  21789  ustuqtop2  21793  ustuqtop3  21794  utop3cls  21802  utopreg  21803  isucn2  21830  met1stc  22072  metustsym  22106  metuel2  22116  xrge0tsms  22372  xmetdcn2  22375  nmoleub2lem2  22650  iscfil2  22785  iscfil3  22792  dvmptfsum  23454  dvlip2  23474  aannenlem1  23799  ulm2  23855  ulmuni  23862  mtestbdd  23875  efopn  24116  dchrptlem1  24701  pntpbnd  24989  pntibnd  24994  f1otrg  25464  f1otrge  25465  pthdepisspth  25865  usgra2adedgwlkonALT  25905  cusconngra  25965  clwlkisclwwlklem2a4  26073  xrofsup  28724  ressprs  28787  omndmul2  28844  isarchi3  28873  archirngz  28875  lmodslmd  28889  gsummpt2d  28913  xrge0tsmsd  28917  suborng  28947  isarchiofld  28949  sqsscirc1  29083  lmxrge0  29127  lmdvg  29128  esumrnmpt2  29258  esumfsup  29260  esumcvg  29276  esum2d  29283  ddemeas  29427  omssubadd  29490  btwnconn1lem13  31177  matunitlindflem1  32373  matunitlindflem2  32374  poimirlem29  32406  mblfinlem3  32416  mblfinlem4  32417  ftc1anclem7  32459  ftc1anc  32461  prdstotbnd  32561  ltrnid  34237  rencldnfilem  36200  pellex  36215  pellfundex  36266  dvdsacongtr  36367  fnchoice  38009  climsuse  38474  addlimc  38514  0ellimcdiv  38515  limclner  38517  icccncfext  38572  dvnprodlem3  38637  fourierdlem12  38811  fourierdlem34  38833  fourierdlem50  38848  fourierdlem80  38878  fourierdlem81  38879  fourierdlem87  38885  etransclem35  38961  sge0pr  39086  smfmullem3  39477  nbupgr  40563  usgr2pth  40967  clwlkclwwlklem2a4  41203  cusconngr  41355  uzlidlring  41716  2zlidl  41721
  Copyright terms: Public domain W3C validator