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

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

Proof of Theorem simp21r
StepHypRef Expression
1 simp1r 1238 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant2 1128 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  modexp  13185  segconeu  32416  4atlem10  35387  lplncvrlvol2  35396  4atex  35857  4atex2-0cOLDN  35861  cdleme0moN  36007  cdleme16e  36064  cdleme17d1  36071  cdleme18d  36077  cdleme19d  36088  cdleme20f  36096  cdleme20g  36097  cdleme21ct  36111  cdleme22aa  36121  cdleme22cN  36124  cdleme22d  36125  cdleme22e  36126  cdleme22eALTN  36127  cdleme26e  36141  cdleme32e  36227  cdleme32f  36228  cdlemg4  36399  cdlemg18d  36463  cdlemg18  36464  cdlemg19a  36465  cdlemg19  36466  cdlemg21  36468  cdlemg33b0  36483  cdlemk5  36618  cdlemk6  36619  cdlemk7  36630  cdlemk11  36631  cdlemk12  36632  cdlemk21N  36655  cdlemk20  36656  cdlemk28-3  36690  cdlemk34  36692  cdlemkfid3N  36707  cdlemk55u1  36747
  Copyright terms: Public domain W3C validator