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

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

Proof of Theorem simp1l2
StepHypRef Expression
1 simpl2 1229 . 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  pmatcollpw2  20803  btwnconn1lem4  32534  linethru  32597  hlrelat3  35220  cvrval3  35221  cvrval4N  35222  2atlt  35247  atbtwnex  35256  1cvratlt  35282  atcvrlln2  35327  atcvrlln  35328  2llnmat  35332  lvolnlelpln  35393  lnjatN  35588  lncmp  35591  cdlemd9  36015  dihord5b  37069  dihmeetALTN  37137  mapdrvallem2  37455
 Copyright terms: Public domain W3C validator