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

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

Proof of Theorem simp32l
StepHypRef Expression
1 simp2l 1199 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant3 1135 1 ((𝜏𝜂 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  cdlema1N  38467  paddasslem15  38510  4atex2-0aOLDN  38754  4atex3  38757  trlval3  38863  cdleme12  38947  cdleme19b  38980  cdleme19d  38982  cdleme19e  38983  cdleme20d  38988  cdleme20f  38990  cdleme20g  38991  cdleme21d  39006  cdleme21e  39007  cdleme21f  39008  cdleme22cN  39018  cdleme22e  39020  cdleme22f2  39023  cdleme22g  39024  cdleme26e  39035  cdleme28a  39046  cdleme37m  39138  cdleme39n  39142  cdlemg28b  39379  cdlemk3  39509  cdlemk12  39526  cdlemk12u  39548  cdlemkoatnle-2N  39551  cdlemk13-2N  39552  cdlemkole-2N  39553  cdlemk14-2N  39554  cdlemk15-2N  39555  cdlemk16-2N  39556  cdlemk17-2N  39557  cdlemk18-2N  39562  cdlemk19-2N  39563  cdlemk7u-2N  39564  cdlemk11u-2N  39565  cdlemk20-2N  39568  cdlemk30  39570  cdlemk23-3  39578  cdlemk24-3  39579
  Copyright terms: Public domain W3C validator