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

Theorem simp-4l 805
 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 797 . 2 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
21adantr 481 1 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  simp-5l  807  marypha1lem  8324  acndom2  8862  ttukeylem6  9321  fpwwe2lem12  9448  reuccats1  13462  dfgcd2  15244  ramcl  15714  initoeu2lem1  16645  gsmsymgreqlem2  17832  dfod2  17962  pgpfi  18001  ghmcyg  18278  psgndif  19929  scmatmulcl  20305  cpmatmcllem  20504  neiptoptop  20916  cncnp  21065  subislly  21265  ptcnplem  21405  pthaus  21422  xkohaus  21437  kqreglem1  21525  cnextcn  21852  qustgplem  21905  trust  22014  utoptop  22019  restutopopn  22023  ustuqtop2  22027  ustuqtop3  22028  utop3cls  22036  utopreg  22037  isucn2  22064  met1stc  22307  metustsym  22341  metuel2  22351  xrge0tsms  22618  xmetdcn2  22621  nmoleub2lem2  22897  iscfil2  23045  iscfil3  23052  dvmptfsum  23719  dvlip2  23739  aannenlem1  24064  ulm2  24120  ulmuni  24127  mtestbdd  24140  efopn  24385  dchrptlem1  24970  pntpbnd  25258  pntibnd  25263  f1otrg  25732  f1otrge  25733  nbupgr  26221  upgriswlk  26518  usgr2pth  26641  clwlkclwwlklem2a4  26879  cusconngr  27031  xrofsup  29507  ressprs  29629  omndmul2  29686  isarchi3  29715  archirngz  29717  lmodslmd  29731  gsummpt2d  29755  xrge0tsmsd  29759  suborng  29789  isarchiofld  29791  sqsscirc1  29928  lmxrge0  29972  lmdvg  29973  esumrnmpt2  30104  esumfsup  30106  esumcvg  30122  esum2d  30129  ddemeas  30273  omssubadd  30336  noetalem3  31839  btwnconn1lem13  32181  matunitlindflem1  33376  matunitlindflem2  33377  poimirlem29  33409  mblfinlem3  33419  mblfinlem4  33420  ftc1anclem7  33462  ftc1anc  33464  prdstotbnd  33564  ltrnid  35240  rencldnfilem  37203  pellex  37218  pellfundex  37269  dvdsacongtr  37370  fnchoice  39008  climsuse  39640  addlimc  39680  0ellimcdiv  39681  limclner  39683  icccncfext  39863  dvnprodlem3  39926  fourierdlem12  40099  fourierdlem34  40121  fourierdlem50  40136  fourierdlem80  40166  fourierdlem81  40167  fourierdlem87  40173  etransclem35  40249  sge0pr  40374  smfmullem3  40763  mogoldbb  41438  uzlidlring  41694  2zlidl  41699
 Copyright terms: Public domain W3C validator