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

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

Proof of Theorem simp1l2
StepHypRef Expression
1 simpl2 1058 . 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  pmatcollpw2  20402  btwnconn1lem4  31367  linethru  31430  hlrelat3  33716  cvrval3  33717  cvrval4N  33718  2atlt  33743  atbtwnex  33752  1cvratlt  33778  atcvrlln2  33823  atcvrlln  33824  2llnmat  33828  lvolnlelpln  33889  lnjatN  34084  lncmp  34087  cdlemd9  34511  dihord5b  35566  dihmeetALTN  35634  mapdrvallem2  35952
  Copyright terms: Public domain W3C validator