Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1l1 Structured version   Visualization version   GIF version

Theorem simp1l1 1350
 Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp1l1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)

Proof of Theorem simp1l1
StepHypRef Expression
1 simpl1 1227 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
213ad2ant1 1127 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071 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  df-3an 1073 This theorem is referenced by:  mapxpen  8282  lsmcv  19355  archiabl  30092  trisegint  32472  linethru  32597  hlrelat3  35220  cvrval3  35221  cvrval4N  35222  2atlt  35247  atbtwnex  35256  1cvratlt  35282  atcvrlln2  35327  atcvrlln  35328  2llnmat  35332  lplnexllnN  35372  lvolnlelpln  35393  lnjatN  35588  lncvrat  35590  lncmp  35591  cdlemd9  36015  dihord5b  37069  dihmeetALTN  37137  dih1dimatlem0  37138  mapdrvallem2  37455
 Copyright terms: Public domain W3C validator