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

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

Proof of Theorem simp1ll
StepHypRef Expression
1 simpll 765 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant1 1130 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084
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 206  df-an 395  df-3an 1086
This theorem is referenced by:  lspsolvlem  21035  1marepvsma1  22503  mdetunilem8  22539  madutpos  22562  ax5seg  28767  rabfodom  32319  measinblem  33844  btwnconn1lem2  35689  btwnconn1lem13  35700  athgt  38933  llnle  38995  lplnle  39017  lhpexle1  39485  lhpj1  39499  lhpat3  39523  ltrncnv  39623  cdleme16aN  39736  tendoicl  40273  cdlemk55b  40437  dihatexv  40815  dihglblem6  40817  limccog  45010  icccncfext  45277  stoweidlem31  45421  stoweidlem34  45424  stoweidlem49  45439  stoweidlem57  45447
  Copyright terms: Public domain W3C validator