Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-5l Structured version   Visualization version   GIF version

Theorem simp-5l 764
 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 708 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 197  df-an 383 This theorem is referenced by:  simp-6lOLD  769  mhmmnd  17744  neiptopnei  21156  neitx  21630  ustex3sym  22240  restutop  22260  ustuqtop4  22267  utopreg  22275  xrge0tsms  22856  f1otrg  25971  xrge0tsmsd  30119  pstmxmet  30274  esumfsup  30466  esum2dlem  30488  esum2d  30489  omssubadd  30696  eulerpartlemgvv  30772  matunitlindflem2  33732  eldioph2  37844  limcrecl  40373  icccncfext  40612  ioodvbdlimc1lem2  40659  ioodvbdlimc2lem  40661  stoweidlem60  40788  fourierdlem77  40911  fourierdlem80  40914  fourierdlem103  40937  fourierdlem104  40938  etransclem35  40997
 Copyright terms: Public domain W3C validator