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

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

Proof of Theorem simp1ll
StepHypRef Expression
1 simpll 786 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant1 1075 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  lspsolvlem  18963  1marepvsma1  20208  mdetunilem8  20244  madutpos  20267  ax5seg  25618  rabfodom  28728  measinblem  29610  btwnconn1lem2  31365  btwnconn1lem13  31376  athgt  33760  llnle  33822  lplnle  33844  lhpexle1  34312  lhpj1  34326  lhpat3  34350  ltrncnv  34450  cdleme16aN  34564  tendoicl  35102  cdlemk55b  35266  dihatexv  35645  dihglblem6  35647  limccog  38687  icccncfext  38773  stoweidlem31  38924  stoweidlem34  38927  stoweidlem49  38942  stoweidlem57  38950
  Copyright terms: Public domain W3C validator