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 781
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 730 1 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  mhmmnd  18159  neiptopnei  21668  neitx  22143  ustex3sym  22753  restutop  22773  ustuqtop4  22780  utopreg  22788  xrge0tsms  23369  f1otrg  26584  nn0xmulclb  30422  xrge0tsmsd  30619  imaslmod  30849  qsidomlem1  30882  extdg1id  30952  pstmxmet  31036  esumfsup  31228  esum2dlem  31250  esum2d  31251  omssubadd  31457  eulerpartlemgvv  31533  signstfvneq0  31741  satffunlem2lem1  32548  matunitlindflem2  34770  dffltz  39149  eldioph2  39237  limcrecl  41786  icccncfext  42046  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  stoweidlem60  42222  fourierdlem77  42345  fourierdlem80  42348  fourierdlem103  42371  fourierdlem104  42372  etransclem35  42431
  Copyright terms: Public domain W3C validator