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

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

Proof of Theorem simp21l
StepHypRef Expression
1 simp1l 1194 . 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:  modexp  13599  segconeu  33586  4atlem10  36901  lplncvrlvol2  36910  4atex  37371  4atex2-0cOLDN  37375  cdlemd2  37494  cdlemd3  37495  cdlemd4  37496  cdleme0e  37512  cdleme0moN  37520  cdleme3g  37529  cdleme3h  37530  cdleme3  37532  cdleme9  37548  cdleme11c  37556  cdleme11dN  37557  cdleme11e  37558  cdleme11fN  37559  cdleme11h  37561  cdleme11j  37562  cdleme11k  37563  cdleme11  37565  cdleme12  37566  cdleme13  37567  cdleme14  37568  cdleme15a  37569  cdleme15b  37570  cdleme15c  37571  cdleme15d  37572  cdleme15  37573  cdleme16b  37574  cdleme16c  37575  cdleme16d  37576  cdleme16e  37577  cdleme16f  37578  cdleme17d1  37584  cdleme18a  37586  cdleme18b  37587  cdleme18c  37588  cdleme18d  37590  cdleme19b  37599  cdleme19d  37601  cdleme19e  37602  cdleme20c  37606  cdleme20d  37607  cdleme20e  37608  cdleme20f  37609  cdleme20g  37610  cdleme20h  37611  cdleme20j  37613  cdleme20l2  37616  cdleme20l  37617  cdleme20m  37618  cdleme20  37619  cdleme21ct  37624  cdleme21e  37626  cdleme21i  37630  cdleme22aa  37634  cdleme22cN  37637  cdleme22d  37638  cdleme22e  37639  cdleme22eALTN  37640  cdleme22f  37641  cdleme26e  37654  cdleme27a  37662  cdleme32e  37740  cdlemg2fv2  37895  cdlemg4a  37903  cdlemg4d  37908  cdlemg4  37912  cdlemg6c  37915  cdlemg8b  37923  cdlemg8c  37924  cdlemg9a  37927  cdlemg9  37929  cdlemg12a  37938  cdlemg12c  37940  cdlemg17dALTN  37959  cdlemg17h  37963  cdlemg18b  37974  cdlemg18c  37975  cdlemg18d  37976  cdlemg18  37977  cdlemg19a  37978  cdlemg21  37981  cdlemg28a  37988  cdlemg31b0a  37990  cdlemg31d  37995  cdlemg33b0  37996  cdlemg33a  38001  cdlemh  38112  cdlemk5  38131  cdlemk6  38132  cdlemk7  38143  cdlemk11  38144  cdlemk12  38145  cdlemk21N  38168  cdlemk20  38169  cdlemk28-3  38203  cdlemk34  38205  cdlemkfid3N  38220  cdlemk35s-id  38233  cdlemk39s-id  38235  cdlemk55u1  38260  cdlemn2  38490  cdlemn10  38501  dihjustlem  38511
  Copyright terms: Public domain W3C validator