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

Theorem simp-4l 823
 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 813 . 2 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
21adantr 480 1 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  simp-5l  825  marypha1lem  8380  acndom2  8915  ttukeylem6  9374  fpwwe2lem12  9501  reuccats1  13526  dfgcd2  15310  ramcl  15780  initoeu2lem1  16711  gsmsymgreqlem2  17897  dfod2  18027  pgpfi  18066  ghmcyg  18343  psgndif  19996  scmatmulcl  20372  cpmatmcllem  20571  neiptoptop  20983  cncnp  21132  subislly  21332  ptcnplem  21472  pthaus  21489  xkohaus  21504  kqreglem1  21592  cnextcn  21918  qustgplem  21971  trust  22080  utoptop  22085  restutopopn  22089  ustuqtop2  22093  ustuqtop3  22094  utop3cls  22102  utopreg  22103  isucn2  22130  met1stc  22373  metustsym  22407  metuel2  22417  xrge0tsms  22684  xmetdcn2  22687  nmoleub2lem2  22962  iscfil2  23110  iscfil3  23117  dvmptfsum  23783  dvlip2  23803  aannenlem1  24128  ulm2  24184  ulmuni  24191  mtestbdd  24204  efopn  24449  dchrptlem1  25034  pntpbnd  25322  pntibnd  25327  f1otrg  25796  f1otrge  25797  nbupgr  26285  upgriswlk  26593  usgr2pth  26716  clwlkclwwlklem2a4  26963  cusconngr  27169  xrofsup  29661  ressprs  29783  omndmul2  29840  isarchi3  29869  archirngz  29871  lmodslmd  29885  gsummpt2d  29909  xrge0tsmsd  29913  suborng  29943  isarchiofld  29945  sqsscirc1  30082  lmxrge0  30126  lmdvg  30127  esumrnmpt2  30258  esumfsup  30260  esumcvg  30276  esum2d  30283  ddemeas  30427  omssubadd  30490  noetalem3  31990  btwnconn1lem13  32331  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem29  33568  mblfinlem3  33578  mblfinlem4  33579  ftc1anclem7  33621  ftc1anc  33623  prdstotbnd  33723  ltrnid  35739  rencldnfilem  37701  pellex  37716  pellfundex  37767  dvdsacongtr  37868  fnchoice  39502  climsuse  40158  addlimc  40198  0ellimcdiv  40199  limclner  40201  climxrre  40300  xlimmnfvlem2  40377  xlimpnfvlem2  40381  icccncfext  40418  dvnprodlem3  40481  fourierdlem12  40654  fourierdlem34  40676  fourierdlem50  40691  fourierdlem80  40721  fourierdlem81  40722  fourierdlem87  40728  etransclem35  40804  sge0pr  40929  meaiuninc3v  41019  smfmullem3  41321  mogoldbb  41998  uzlidlring  42254  2zlidl  42259
 Copyright terms: Public domain W3C validator