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

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

Proof of Theorem simp32r
StepHypRef Expression
1 simp2r 1243 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant3 1130 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:  cdlema1N  35598  paddasslem15  35641  4atex2-0aOLDN  35885  4atex3  35888  cdleme19b  36112  cdleme19d  36114  cdleme19e  36115  cdleme20d  36120  cdleme20f  36122  cdleme20g  36123  cdleme21d  36138  cdleme21e  36139  cdleme22cN  36150  cdleme22e  36152  cdleme22f2  36155  cdleme26e  36167  cdleme28a  36178  cdleme37m  36270  cdlemg28b  36511  cdlemk3  36641  cdlemk12  36658  cdlemk12u  36680  cdlemkoatnle-2N  36683  cdlemk13-2N  36684  cdlemkole-2N  36685  cdlemk14-2N  36686  cdlemk15-2N  36687  cdlemk16-2N  36688  cdlemk17-2N  36689  cdlemk18-2N  36694  cdlemk19-2N  36695  cdlemk7u-2N  36696  cdlemk11u-2N  36697  cdlemk20-2N  36700  cdlemk30  36702  cdlemk23-3  36710  cdlemk24-3  36711
  Copyright terms: Public domain W3C validator