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

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

Proof of Theorem simp1ll
StepHypRef Expression
1 simpll 789 . 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:  lspsolvlem  19061  1marepvsma1  20308  mdetunilem8  20344  madutpos  20367  ax5seg  25718  rabfodom  29191  measinblem  30064  btwnconn1lem2  31837  btwnconn1lem13  31848  athgt  34222  llnle  34284  lplnle  34306  lhpexle1  34774  lhpj1  34788  lhpat3  34812  ltrncnv  34912  cdleme16aN  35026  tendoicl  35564  cdlemk55b  35728  dihatexv  36107  dihglblem6  36109  limccog  39256  icccncfext  39404  stoweidlem31  39555  stoweidlem34  39558  stoweidlem49  39573  stoweidlem57  39581
  Copyright terms: Public domain W3C validator