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

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

Proof of Theorem simp32r
StepHypRef Expression
1 simp2r 1198 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant3 1133 1 ((𝜏𝜂 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085
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 396  df-3an 1087
This theorem is referenced by:  cdlema1N  39201  paddasslem15  39244  4atex2-0aOLDN  39488  4atex3  39491  cdleme19b  39714  cdleme19d  39716  cdleme19e  39717  cdleme20d  39722  cdleme20f  39724  cdleme20g  39725  cdleme21d  39740  cdleme21e  39741  cdleme22cN  39752  cdleme22e  39754  cdleme22f2  39757  cdleme26e  39769  cdleme28a  39780  cdleme37m  39872  cdlemg28b  40113  cdlemk3  40243  cdlemk12  40260  cdlemk12u  40282  cdlemkoatnle-2N  40285  cdlemk13-2N  40286  cdlemkole-2N  40287  cdlemk14-2N  40288  cdlemk15-2N  40289  cdlemk16-2N  40290  cdlemk17-2N  40291  cdlemk18-2N  40296  cdlemk19-2N  40297  cdlemk7u-2N  40298  cdlemk11u-2N  40299  cdlemk20-2N  40302  cdlemk30  40304  cdlemk23-3  40312  cdlemk24-3  40313
  Copyright terms: Public domain W3C validator