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

Theorem simp2ll 1241
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 1135 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  tfrlem5  8330  omeu  8536  expmordi  14081  4sqlem18  16842  vdwlem10  16870  0catg  17576  mvrf1  21417  mdetuni0  21993  mdetmul  21995  tsmsxp  23529  ax5seglem3  27929  btwnconn1lem1  34725  btwnconn1lem2  34726  btwnconn1lem3  34727  btwnconn1lem12  34736  btwnconn1lem13  34737  lshpkrlem6  37627  athgt  37969  2llnjN  38080  dalaw  38399  lhpmcvr4N  38539  cdlemb2  38554  4atexlemex6  38587  cdlemd7  38717  cdleme01N  38734  cdleme02N  38735  cdleme0ex1N  38736  cdleme0ex2N  38737  cdleme7aa  38755  cdleme7c  38758  cdleme7d  38759  cdleme7e  38760  cdleme7ga  38761  cdleme7  38762  cdleme11a  38773  cdleme20k  38832  cdleme27cl  38879  cdleme42e  38992  cdleme42h  38995  cdleme42i  38996  cdlemf  39076  cdlemg2kq  39115  cdlemg2m  39117  cdlemg8a  39140  cdlemg11aq  39151  cdlemg10c  39152  cdlemg11b  39155  cdlemg17a  39174  cdlemg31b0N  39207  cdlemg31c  39212  cdlemg33c0  39215  cdlemg41  39231  cdlemh2  39329  cdlemn9  39718  dihglbcpreN  39813  dihmeetlem3N  39818  dihmeetlem13N  39832  pellex  41205
  Copyright terms: Public domain W3C validator