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 766 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant1 1130 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃𝜏) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  lspsolvlem  19905  1marepvsma1  21186  mdetunilem8  21222  madutpos  21245  ax5seg  26730  rabfodom  30272  measinblem  31553  btwnconn1lem2  33623  btwnconn1lem13  33634  athgt  36710  llnle  36772  lplnle  36794  lhpexle1  37262  lhpj1  37276  lhpat3  37300  ltrncnv  37400  cdleme16aN  37513  tendoicl  38050  cdlemk55b  38214  dihatexv  38592  dihglblem6  38594  limccog  42201  icccncfext  42468  stoweidlem31  42612  stoweidlem34  42615  stoweidlem49  42630  stoweidlem57  42638
 Copyright terms: Public domain W3C validator