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

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

Proof of Theorem simp32l
StepHypRef Expression
1 simp2l 1085 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant3 1082 1 ((𝜏𝜂 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  cdlema1N  34596  paddasslem15  34639  4atex2-0aOLDN  34883  4atex3  34886  trlval3  34993  cdleme12  35077  cdleme19b  35111  cdleme19d  35113  cdleme19e  35114  cdleme20d  35119  cdleme20f  35121  cdleme20g  35122  cdleme21d  35137  cdleme21e  35138  cdleme21f  35139  cdleme22cN  35149  cdleme22e  35151  cdleme22f2  35154  cdleme22g  35155  cdleme26e  35166  cdleme28a  35177  cdleme37m  35269  cdleme39n  35273  cdlemg28b  35510  cdlemk3  35640  cdlemk12  35657  cdlemk12u  35679  cdlemkoatnle-2N  35682  cdlemk13-2N  35683  cdlemkole-2N  35684  cdlemk14-2N  35685  cdlemk15-2N  35686  cdlemk16-2N  35687  cdlemk17-2N  35688  cdlemk18-2N  35693  cdlemk19-2N  35694  cdlemk7u-2N  35695  cdlemk11u-2N  35696  cdlemk20-2N  35699  cdlemk30  35701  cdlemk23-3  35709  cdlemk24-3  35710
  Copyright terms: Public domain W3C validator