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

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

Proof of Theorem simp32l
StepHypRef Expression
1 simp2l 1196 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant3 1132 1 ((𝜏𝜂 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  cdlema1N  36999  paddasslem15  37042  4atex2-0aOLDN  37286  4atex3  37289  trlval3  37395  cdleme12  37479  cdleme19b  37512  cdleme19d  37514  cdleme19e  37515  cdleme20d  37520  cdleme20f  37522  cdleme20g  37523  cdleme21d  37538  cdleme21e  37539  cdleme21f  37540  cdleme22cN  37550  cdleme22e  37552  cdleme22f2  37555  cdleme22g  37556  cdleme26e  37567  cdleme28a  37578  cdleme37m  37670  cdleme39n  37674  cdlemg28b  37911  cdlemk3  38041  cdlemk12  38058  cdlemk12u  38080  cdlemkoatnle-2N  38083  cdlemk13-2N  38084  cdlemkole-2N  38085  cdlemk14-2N  38086  cdlemk15-2N  38087  cdlemk16-2N  38088  cdlemk17-2N  38089  cdlemk18-2N  38094  cdlemk19-2N  38095  cdlemk7u-2N  38096  cdlemk11u-2N  38097  cdlemk20-2N  38100  cdlemk30  38102  cdlemk23-3  38110  cdlemk24-3  38111
  Copyright terms: Public domain W3C validator