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

Theorem simp-5l 785
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
Assertion
Ref Expression
simp-5l ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)

Proof of Theorem simp-5l
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
21ad5antr 734 1 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  mhmmnd  19082  neiptopnei  23140  neitx  23615  ustex3sym  24226  restutop  24246  ustuqtop4  24253  utopreg  24261  xrge0tsms  24856  noetainflem4  27785  f1otrg  28879  nn0xmulclb  32775  xrge0tsmsd  33065  elrgspnlem4  33249  imaslmod  33381  elrspunidl  33456  rhmpreimaprmidl  33479  qsidomlem1  33480  mxidlprm  33498  1arithidom  33565  dfufd2  33578  extdg1id  33716  pstmxmet  33896  esumfsup  34071  esum2dlem  34093  esum2d  34094  omssubadd  34302  eulerpartlemgvv  34378  signstfvneq0  34587  satffunlem2lem1  35409  matunitlindflem2  37624  aks6d1c2p2  42120  dffltz  42644  eldioph2  42773  limcrecl  45644  icccncfext  45902  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem60  46075  fourierdlem77  46198  fourierdlem80  46201  fourierdlem103  46224  fourierdlem104  46225  etransclem35  46284
  Copyright terms: Public domain W3C validator