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

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

Proof of Theorem simp1l2
StepHypRef Expression
1 simpl2 1063 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
213ad2ant1 1080 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  mapxpen  8070  lsmcv  19060  pmatcollpw2  20502  btwnconn1lem4  31836  linethru  31899  hlrelat3  34175  cvrval3  34176  cvrval4N  34177  2atlt  34202  atbtwnex  34211  1cvratlt  34237  atcvrlln2  34282  atcvrlln  34283  2llnmat  34287  lvolnlelpln  34348  lnjatN  34543  lncmp  34546  cdlemd9  34970  dihord5b  36025  dihmeetALTN  36093  mapdrvallem2  36411
  Copyright terms: Public domain W3C validator