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

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

Proof of Theorem simp1l2
StepHypRef Expression
1 simpl2 1186 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
213ad2ant1 1127 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  mapxpen  8675  lsmcv  19835  pmatcollpw2  21304  btwnconn1lem4  33437  linethru  33500  hlrelat3  36417  cvrval3  36418  cvrval4N  36419  2atlt  36444  atbtwnex  36453  1cvratlt  36479  atcvrlln2  36524  atcvrlln  36525  2llnmat  36529  lvolnlelpln  36590  lnjatN  36785  lncmp  36788  cdlemd9  37211  dihord5b  38264  dihmeetALTN  38332  mapdrvallem2  38650  itschlc0xyqsol  44588
  Copyright terms: Public domain W3C validator