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 807
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 805 . 2 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
21adantr 481 1 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  simp-6l  809  mhmmnd  17518  neiptopnei  20917  neitx  21391  ustex3sym  22002  restutop  22022  ustuqtop4  22029  utopreg  22037  xrge0tsms  22618  f1otrg  25732  xrge0tsmsd  29759  pstmxmet  29914  esumfsup  30106  esum2dlem  30128  esum2d  30129  omssubadd  30336  eulerpartlemgvv  30412  matunitlindflem2  33377  eldioph2  37144  limcrecl  39661  icccncfext  39863  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  stoweidlem60  40040  fourierdlem77  40163  fourierdlem80  40166  fourierdlem103  40189  fourierdlem104  40190  etransclem35  40249
  Copyright terms: Public domain W3C validator