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

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

Proof of Theorem simp22r
StepHypRef Expression
1 simp2r 1197 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant2 1131 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:  ax5seglem6  26726  frrlem10  33206  segconeu  33546  3atlem2  36738  lplnexllnN  36818  lplncvrlvol2  36869  4atex  37330  cdleme3g  37488  cdleme3h  37489  cdleme11h  37520  cdleme20bN  37564  cdleme20c  37565  cdleme20f  37568  cdleme20g  37569  cdleme20j  37572  cdleme20l2  37575  cdleme20l  37576  cdleme21ct  37583  cdleme26e  37613  cdleme43fsv1snlem  37674  cdleme39n  37720  cdleme40m  37721  cdleme42k  37738  cdlemg6c  37874  cdlemg31d  37954  cdlemg33a  37960  cdlemg33c  37962  cdlemg33d  37963  cdlemg33e  37964  cdlemg33  37965  cdlemh  38071  cdlemk7u-2N  38142  cdlemk11u-2N  38143  cdlemk12u-2N  38144  cdlemk20-2N  38146  cdlemk28-3  38162  cdlemk33N  38163  cdlemk34  38164  cdlemk39  38170  cdlemkyyN  38216
  Copyright terms: Public domain W3C validator