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 803
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 801 . 2 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
21adantr 479 1 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  simp-6l  805  mhmmnd  17301  neiptopnei  20683  neitx  21157  ustex3sym  21768  restutop  21788  ustuqtop4  21795  utopreg  21803  xrge0tsms  22372  f1otrg  25464  usg2spot2nb  26353  xrge0tsmsd  28917  pstmxmet  29069  esumfsup  29260  esum2dlem  29282  esum2d  29283  omssubadd  29490  eulerpartlemgvv  29566  matunitlindflem2  32374  eldioph2  36141  limcrecl  38495  icccncfext  38572  ioodvbdlimc1lem2  38621  ioodvbdlimc2lem  38623  stoweidlem60  38752  fourierdlem77  38875  fourierdlem80  38878  fourierdlem103  38901  fourierdlem104  38902  etransclem35  38961
  Copyright terms: Public domain W3C validator