MPE Home 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