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 767 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant2 1135 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  tfrlem5  8420  omeu  8623  expmordi  14207  hash7g  14525  4sqlem18  17000  vdwlem10  17028  0catg  17731  mvrf1  22006  mdetuni0  22627  mdetmul  22629  tsmsxp  24163  ax5seglem3  28946  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem3  36090  btwnconn1lem12  36099  btwnconn1lem13  36100  lshpkrlem6  39116  athgt  39458  2llnjN  39569  dalaw  39888  lhpmcvr4N  40028  cdlemb2  40043  4atexlemex6  40076  cdlemd7  40206  cdleme01N  40223  cdleme02N  40224  cdleme0ex1N  40225  cdleme0ex2N  40226  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme11a  40262  cdleme20k  40321  cdleme27cl  40368  cdleme42e  40481  cdleme42h  40484  cdleme42i  40485  cdlemf  40565  cdlemg2kq  40604  cdlemg2m  40606  cdlemg8a  40629  cdlemg11aq  40640  cdlemg10c  40641  cdlemg11b  40644  cdlemg17a  40663  cdlemg31b0N  40696  cdlemg31c  40701  cdlemg33c0  40704  cdlemg41  40720  cdlemh2  40818  cdlemn9  41207  dihglbcpreN  41302  dihmeetlem3N  41307  dihmeetlem13N  41321  pellex  42846
  Copyright terms: Public domain W3C validator