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 782
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
Assertion
Ref Expression
simp-4l (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simp-4l
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
21ad4antr 731 1 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  marypha1lem  8885  acndom2  9469  ttukeylem6  9929  fpwwe2lem12  10056  swrdccatin1  14082  dfgcd2  15887  ramcl  16358  initoeu2lem1  17269  initoeu2  17271  gsmsymgreqlem2  18554  dfod2  18686  pgpfi  18725  ghmcyg  19012  psgndif  20294  scmatmulcl  21126  cpmatmcllem  21326  neiptoptop  21739  cncnp  21888  subislly  22089  ptcnplem  22229  pthaus  22246  xkohaus  22261  kqreglem1  22349  cnextcn  22675  qustgplem  22729  trust  22838  utoptop  22843  restutopopn  22847  utop3cls  22860  utopreg  22861  isucn2  22888  met1stc  23131  metustsym  23165  metuel2  23175  xrge0tsms  23442  xmetdcn2  23445  nmoleub2lem2  23724  iscfil2  23873  iscfil3  23880  dvmptfsum  24581  dvlip2  24601  aannenlem1  24927  ulm2  24983  ulmuni  24990  mtestbdd  25003  efopn  25252  dchrptlem1  25851  pntpbnd  26175  pntibnd  26180  f1otrg  26668  nbupgr  27137  upgriswlk  27433  usgr2pth  27556  clwwlkccatlem  27777  clwlkclwwlklem2a4  27785  cusconngr  27979  xrofsup  30521  ressprs  30671  gsummpt2d  30737  xrge0tsmsd  30745  omndmul2  30766  trsp2cyc  30818  isarchi3  30869  archirngz  30871  lmodslmd  30885  suborng  30942  isarchiofld  30944  rhmpreimaidl  31014  dimkerim  31111  sqsscirc1  31259  lmxrge0  31303  lmdvg  31304  esumrnmpt2  31435  esumfsup  31437  esumcvg  31453  esum2d  31460  ddemeas  31603  omssubadd  31666  satffunlem1lem1  32757  satffunlem2lem1  32759  noetalem3  33327  btwnconn1lem13  33668  matunitlindflem1  35046  matunitlindflem2  35047  poimirlem29  35079  mblfinlem3  35089  mblfinlem4  35090  ftc1anclem7  35129  ftc1anc  35131  prdstotbnd  35225  ltrnid  37424  rencldnfilem  39748  pellex  39763  pellfundex  39814  dvdsacongtr  39912  fnchoice  41645  climsuse  42237  addlimc  42277  0ellimcdiv  42278  climxrre  42379  xlimmnfvlem2  42462  xlimpnfvlem2  42466  icccncfext  42516  dvnprodlem3  42577  fourierdlem12  42748  fourierdlem34  42770  fourierdlem50  42785  fourierdlem80  42815  fourierdlem81  42816  fourierdlem87  42822  etransclem35  42898  sge0pr  43020  meaiuninc3v  43110  smfmullem3  43412  mogoldbb  44290  uzlidlring  44540  2zlidl  44545
  Copyright terms: Public domain W3C validator