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

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

Proof of Theorem simp21l
StepHypRef Expression
1 simp1l 1083 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
213ad2ant2 1081 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  modexp  12947  segconeu  31795  4atlem10  34407  lplncvrlvol2  34416  4atex  34877  4atex2-0cOLDN  34881  cdlemd2  35001  cdlemd3  35002  cdlemd4  35003  cdleme0e  35019  cdleme0moN  35027  cdleme3g  35036  cdleme3h  35037  cdleme3  35039  cdleme9  35055  cdleme11c  35063  cdleme11dN  35064  cdleme11e  35065  cdleme11fN  35066  cdleme11h  35068  cdleme11j  35069  cdleme11k  35070  cdleme11  35072  cdleme12  35073  cdleme13  35074  cdleme14  35075  cdleme15a  35076  cdleme15b  35077  cdleme15c  35078  cdleme15d  35079  cdleme15  35080  cdleme16b  35081  cdleme16c  35082  cdleme16d  35083  cdleme16e  35084  cdleme16f  35085  cdleme17d1  35091  cdleme18a  35093  cdleme18b  35094  cdleme18c  35095  cdleme18d  35097  cdleme19b  35107  cdleme19d  35109  cdleme19e  35110  cdleme20c  35114  cdleme20d  35115  cdleme20e  35116  cdleme20f  35117  cdleme20g  35118  cdleme20h  35119  cdleme20j  35121  cdleme20l2  35124  cdleme20l  35125  cdleme20m  35126  cdleme20  35127  cdleme21ct  35132  cdleme21e  35134  cdleme21i  35138  cdleme22aa  35142  cdleme22cN  35145  cdleme22d  35146  cdleme22e  35147  cdleme22eALTN  35148  cdleme22f  35149  cdleme26e  35162  cdleme27a  35170  cdleme32e  35248  cdlemg2fv2  35403  cdlemg4a  35411  cdlemg4d  35416  cdlemg4  35420  cdlemg6c  35423  cdlemg8b  35431  cdlemg8c  35432  cdlemg9a  35435  cdlemg9  35437  cdlemg12a  35446  cdlemg12c  35448  cdlemg17dALTN  35467  cdlemg17h  35471  cdlemg18b  35482  cdlemg18c  35483  cdlemg18d  35484  cdlemg18  35485  cdlemg19a  35486  cdlemg21  35489  cdlemg28a  35496  cdlemg31b0a  35498  cdlemg31d  35503  cdlemg33b0  35504  cdlemg33a  35509  cdlemh  35620  cdlemk5  35639  cdlemk6  35640  cdlemk7  35651  cdlemk11  35652  cdlemk12  35653  cdlemk21N  35676  cdlemk20  35677  cdlemk28-3  35711  cdlemk34  35713  cdlemkfid3N  35728  cdlemk35s-id  35741  cdlemk39s-id  35743  cdlemk55u1  35768  cdlemn2  35999  cdlemn10  36010  dihjustlem  36020
  Copyright terms: Public domain W3C validator