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

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

Proof of Theorem simp2ll
StepHypRef Expression
1 simpll 766 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant2 1131 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:  tfrlem5  8003  omeu  8198  expmordi  13527  4sqlem18  16287  vdwlem10  16315  0catg  16949  mvrf1  20661  mdetuni0  21224  mdetmul  21226  tsmsxp  22758  ax5seglem3  26723  btwnconn1lem1  33622  btwnconn1lem2  33623  btwnconn1lem3  33624  btwnconn1lem12  33633  btwnconn1lem13  33634  lshpkrlem6  36373  athgt  36714  2llnjN  36825  dalaw  37144  lhpmcvr4N  37284  cdlemb2  37299  4atexlemex6  37332  cdlemd7  37462  cdleme01N  37479  cdleme02N  37480  cdleme0ex1N  37481  cdleme0ex2N  37482  cdleme7aa  37500  cdleme7c  37503  cdleme7d  37504  cdleme7e  37505  cdleme7ga  37506  cdleme7  37507  cdleme11a  37518  cdleme20k  37577  cdleme27cl  37624  cdleme42e  37737  cdleme42h  37740  cdleme42i  37741  cdlemf  37821  cdlemg2kq  37860  cdlemg2m  37862  cdlemg8a  37885  cdlemg11aq  37896  cdlemg10c  37897  cdlemg11b  37900  cdlemg17a  37919  cdlemg31b0N  37952  cdlemg31c  37957  cdlemg33c0  37960  cdlemg41  37976  cdlemh2  38074  cdlemn9  38463  dihglbcpreN  38558  dihmeetlem3N  38563  dihmeetlem13N  38577  pellex  39710
  Copyright terms: Public domain W3C validator