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 733 1 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  mhmmnd  18874  neiptopnei  22499  neitx  22974  ustex3sym  23585  restutop  23605  ustuqtop4  23612  utopreg  23620  xrge0tsms  24213  noetainflem4  27104  f1otrg  27855  nn0xmulclb  31723  xrge0tsmsd  31948  imaslmod  32192  elrspunidl  32251  rhmpreimaprmidl  32272  qsidomlem1  32273  mxidlprm  32285  extdg1id  32409  pstmxmet  32535  esumfsup  32726  esum2dlem  32748  esum2d  32749  omssubadd  32957  eulerpartlemgvv  33033  signstfvneq0  33241  satffunlem2lem1  34055  matunitlindflem2  36121  aks6d1c2p2  40595  dffltz  41015  eldioph2  41128  limcrecl  43956  icccncfext  44214  ioodvbdlimc1lem2  44259  ioodvbdlimc2lem  44261  stoweidlem60  44387  fourierdlem77  44510  fourierdlem80  44513  fourierdlem103  44536  fourierdlem104  44537  etransclem35  44596
  Copyright terms: Public domain W3C validator