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

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

Proof of Theorem simp1ll
StepHypRef Expression
1 simpll 750 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant1 1127 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  lspsolvlem  19356  1marepvsma1  20607  mdetunilem8  20643  madutpos  20666  ax5seg  26039  rabfodom  29682  measinblem  30623  btwnconn1lem2  32532  btwnconn1lem13  32543  athgt  35264  llnle  35326  lplnle  35348  lhpexle1  35816  lhpj1  35830  lhpat3  35854  ltrncnv  35954  cdleme16aN  36068  tendoicl  36605  cdlemk55b  36769  dihatexv  37148  dihglblem6  37150  limccog  40370  icccncfext  40618  stoweidlem31  40765  stoweidlem34  40768  stoweidlem49  40783  stoweidlem57  40791
  Copyright terms: Public domain W3C validator