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

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

Proof of Theorem simp1l1
StepHypRef Expression
1 simpl1 1062 . 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  archiabl  29534  trisegint  31774  linethru  31899  hlrelat3  34175  cvrval3  34176  cvrval4N  34177  2atlt  34202  atbtwnex  34211  1cvratlt  34237  atcvrlln2  34282  atcvrlln  34283  2llnmat  34287  lplnexllnN  34327  lvolnlelpln  34348  lnjatN  34543  lncvrat  34545  lncmp  34546  cdlemd9  34970  dihord5b  36025  dihmeetALTN  36093  dih1dimatlem0  36094  mapdrvallem2  36411
  Copyright terms: Public domain W3C validator