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

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

Proof of Theorem simp22r
StepHypRef Expression
1 simp2r 1192 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant2 1126 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  ax5seglem6  26648  frrlem10  33030  segconeu  33370  3atlem2  36502  lplnexllnN  36582  lplncvrlvol2  36633  4atex  37094  cdleme3g  37252  cdleme3h  37253  cdleme11h  37284  cdleme20bN  37328  cdleme20c  37329  cdleme20f  37332  cdleme20g  37333  cdleme20j  37336  cdleme20l2  37339  cdleme20l  37340  cdleme21ct  37347  cdleme26e  37377  cdleme43fsv1snlem  37438  cdleme39n  37484  cdleme40m  37485  cdleme42k  37502  cdlemg6c  37638  cdlemg31d  37718  cdlemg33a  37724  cdlemg33c  37726  cdlemg33d  37727  cdlemg33e  37728  cdlemg33  37729  cdlemh  37835  cdlemk7u-2N  37906  cdlemk11u-2N  37907  cdlemk12u-2N  37908  cdlemk20-2N  37910  cdlemk28-3  37926  cdlemk33N  37927  cdlemk34  37928  cdlemk39  37934  cdlemkyyN  37980
  Copyright terms: Public domain W3C validator