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

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

Proof of Theorem simp1l1
StepHypRef Expression
1 simpl1 1188 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
213ad2ant1 1130 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  mapxpen  8680  lsmcv  19913  archiabl  30862  trisegint  33549  linethru  33674  hlrelat3  36656  cvrval3  36657  cvrval4N  36658  2atlt  36683  atbtwnex  36692  1cvratlt  36718  atcvrlln2  36763  atcvrlln  36764  2llnmat  36768  lplnexllnN  36808  lvolnlelpln  36829  lnjatN  37024  lncvrat  37026  lncmp  37027  cdlemd9  37450  dihord5b  38503  dihmeetALTN  38571  dih1dimatlem0  38572  mapdrvallem2  38889  grumnudlem  40917
 Copyright terms: Public domain W3C validator