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

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

Proof of Theorem simp1l1
StepHypRef Expression
1 simpl1 1171 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
213ad2ant1 1113 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  w3a 1068
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 199  df-an 388  df-3an 1070
This theorem is referenced by:  mapxpen  8479  lsmcv  19635  archiabl  30499  trisegint  33016  linethru  33141  hlrelat3  35999  cvrval3  36000  cvrval4N  36001  2atlt  36026  atbtwnex  36035  1cvratlt  36061  atcvrlln2  36106  atcvrlln  36107  2llnmat  36111  lplnexllnN  36151  lvolnlelpln  36172  lnjatN  36367  lncvrat  36369  lncmp  36370  cdlemd9  36793  dihord5b  37846  dihmeetALTN  37914  dih1dimatlem0  37915  mapdrvallem2  38232  grumnudlem  40002
  Copyright terms: Public domain W3C validator