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

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

Proof of Theorem simp32r
StepHypRef Expression
1 simp2r 1241 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant3 1128 1 ((𝜏𝜂 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1070 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 383  df-3an 1072 This theorem is referenced by:  cdlema1N  35592  paddasslem15  35635  4atex2-0aOLDN  35879  4atex3  35882  cdleme19b  36106  cdleme19d  36108  cdleme19e  36109  cdleme20d  36114  cdleme20f  36116  cdleme20g  36117  cdleme21d  36132  cdleme21e  36133  cdleme22cN  36144  cdleme22e  36146  cdleme22f2  36149  cdleme26e  36161  cdleme28a  36172  cdleme37m  36264  cdlemg28b  36505  cdlemk3  36635  cdlemk12  36652  cdlemk12u  36674  cdlemkoatnle-2N  36677  cdlemk13-2N  36678  cdlemkole-2N  36679  cdlemk14-2N  36680  cdlemk15-2N  36681  cdlemk16-2N  36682  cdlemk17-2N  36683  cdlemk18-2N  36688  cdlemk19-2N  36689  cdlemk7u-2N  36690  cdlemk11u-2N  36691  cdlemk20-2N  36694  cdlemk30  36696  cdlemk23-3  36704  cdlemk24-3  36705
 Copyright terms: Public domain W3C validator