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

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

Proof of Theorem simp21r
StepHypRef Expression
1 simp1r 1197 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant2 1133 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086
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 397  df-3an 1088
This theorem is referenced by:  modexp  14054  segconeu  34409  4atlem10  37874  lplncvrlvol2  37883  4atex  38344  4atex2-0cOLDN  38348  cdleme0moN  38493  cdleme16e  38550  cdleme17d1  38557  cdleme18d  38563  cdleme19d  38574  cdleme20f  38582  cdleme20g  38583  cdleme21ct  38597  cdleme22aa  38607  cdleme22cN  38610  cdleme22d  38611  cdleme22e  38612  cdleme22eALTN  38613  cdleme26e  38627  cdleme32e  38713  cdleme32f  38714  cdlemg4  38885  cdlemg18d  38949  cdlemg18  38950  cdlemg19a  38951  cdlemg19  38952  cdlemg21  38954  cdlemg33b0  38969  cdlemk5  39104  cdlemk6  39105  cdlemk7  39116  cdlemk11  39117  cdlemk12  39118  cdlemk21N  39141  cdlemk20  39142  cdlemk28-3  39176  cdlemk34  39178  cdlemkfid3N  39193  cdlemk55u1  39233
  Copyright terms: Public domain W3C validator