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

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

Proof of Theorem simp1l1
StepHypRef Expression
1 simpl1 1057 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
213ad2ant1 1075 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  mapxpen  8011  lsmcv  18962  archiabl  29083  trisegint  31305  linethru  31430  hlrelat3  33716  cvrval3  33717  cvrval4N  33718  2atlt  33743  atbtwnex  33752  1cvratlt  33778  atcvrlln2  33823  atcvrlln  33824  2llnmat  33828  lplnexllnN  33868  lvolnlelpln  33889  lnjatN  34084  lncvrat  34086  lncmp  34087  cdlemd9  34511  dihord5b  35566  dihmeetALTN  35634  dih1dimatlem0  35635  mapdrvallem2  35952
  Copyright terms: Public domain W3C validator