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

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

Proof of Theorem simp32r
StepHypRef Expression
1 simp2r 1250 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant3 1158 1 ((𝜏𝜂 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  cdlema1N  35577  paddasslem15  35620  4atex2-0aOLDN  35864  4atex3  35867  cdleme19b  36090  cdleme19d  36092  cdleme19e  36093  cdleme20d  36098  cdleme20f  36100  cdleme20g  36101  cdleme21d  36116  cdleme21e  36117  cdleme22cN  36128  cdleme22e  36130  cdleme22f2  36133  cdleme26e  36145  cdleme28a  36156  cdleme37m  36248  cdlemg28b  36489  cdlemk3  36619  cdlemk12  36636  cdlemk12u  36658  cdlemkoatnle-2N  36661  cdlemk13-2N  36662  cdlemkole-2N  36663  cdlemk14-2N  36664  cdlemk15-2N  36665  cdlemk16-2N  36666  cdlemk17-2N  36667  cdlemk18-2N  36672  cdlemk19-2N  36673  cdlemk7u-2N  36674  cdlemk11u-2N  36675  cdlemk20-2N  36678  cdlemk30  36680  cdlemk23-3  36688  cdlemk24-3  36689
  Copyright terms: Public domain W3C validator