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

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

Proof of Theorem simp21r
StepHypRef Expression
1 simp1r 1084 . 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  12939  segconeu  31757  4atlem10  34369  lplncvrlvol2  34378  4atex  34839  4atex2-0cOLDN  34843  cdleme0moN  34989  cdleme16e  35046  cdleme17d1  35053  cdleme18d  35059  cdleme19d  35071  cdleme20f  35079  cdleme20g  35080  cdleme21ct  35094  cdleme22aa  35104  cdleme22cN  35107  cdleme22d  35108  cdleme22e  35109  cdleme22eALTN  35110  cdleme26e  35124  cdleme32e  35210  cdleme32f  35211  cdlemg4  35382  cdlemg18d  35446  cdlemg18  35447  cdlemg19a  35448  cdlemg19  35449  cdlemg21  35451  cdlemg33b0  35466  cdlemk5  35601  cdlemk6  35602  cdlemk7  35613  cdlemk11  35614  cdlemk12  35615  cdlemk21N  35638  cdlemk20  35639  cdlemk28-3  35673  cdlemk34  35675  cdlemkfid3N  35690  cdlemk55u1  35730
  Copyright terms: Public domain W3C validator