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 784
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  19003  neiptopnei  23026  neitx  23501  ustex3sym  24112  restutop  24132  ustuqtop4  24139  utopreg  24147  xrge0tsms  24730  noetainflem4  27659  f1otrg  28805  nn0xmulclb  32701  xrge0tsmsd  33009  elrgspnlem4  33203  imaslmod  33331  elrspunidl  33406  rhmpreimaprmidl  33429  qsidomlem1  33430  mxidlprm  33448  1arithidom  33515  dfufd2  33528  extdg1id  33668  pstmxmet  33894  esumfsup  34067  esum2dlem  34089  esum2d  34090  omssubadd  34298  eulerpartlemgvv  34374  signstfvneq0  34570  satffunlem2lem1  35398  matunitlindflem2  37618  aks6d1c2p2  42114  dffltz  42629  eldioph2  42757  limcrecl  45634  icccncfext  45892  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem60  46065  fourierdlem77  46188  fourierdlem80  46191  fourierdlem103  46214  fourierdlem104  46215  etransclem35  46274
  Copyright terms: Public domain W3C validator