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 804
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-5l ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)

Proof of Theorem simp-5l
StepHypRef Expression
1 simp-4l 802 . 2 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
21adantr 480 1 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  simp-6l  806  mhmmnd  17360  neiptopnei  20746  neitx  21220  ustex3sym  21831  restutop  21851  ustuqtop4  21858  utopreg  21866  xrge0tsms  22445  f1otrg  25551  usg2spot2nb  26592  xrge0tsmsd  29116  pstmxmet  29268  esumfsup  29459  esum2dlem  29481  esum2d  29482  omssubadd  29689  eulerpartlemgvv  29765  matunitlindflem2  32576  eldioph2  36343  limcrecl  38696  icccncfext  38773  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem60  38953  fourierdlem77  39076  fourierdlem80  39079  fourierdlem103  39102  fourierdlem104  39103  etransclem35  39162
  Copyright terms: Public domain W3C validator