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

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

Proof of Theorem simp22r
StepHypRef Expression
1 simp2r 1201 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant2 1135 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 207  df-an 396  df-3an 1089
This theorem is referenced by:  frrlem10  8320  ttrclselem2  9766  ax5seglem6  28949  segconeu  36012  3atlem2  39486  lplnexllnN  39566  lplncvrlvol2  39617  4atex  40078  cdleme3g  40236  cdleme3h  40237  cdleme11h  40268  cdleme20bN  40312  cdleme20c  40313  cdleme20f  40316  cdleme20g  40317  cdleme20j  40320  cdleme20l2  40323  cdleme20l  40324  cdleme21ct  40331  cdleme26e  40361  cdleme43fsv1snlem  40422  cdleme39n  40468  cdleme40m  40469  cdleme42k  40486  cdlemg6c  40622  cdlemg31d  40702  cdlemg33a  40708  cdlemg33c  40710  cdlemg33d  40711  cdlemg33e  40712  cdlemg33  40713  cdlemh  40819  cdlemk7u-2N  40890  cdlemk11u-2N  40891  cdlemk12u-2N  40892  cdlemk20-2N  40894  cdlemk28-3  40910  cdlemk33N  40911  cdlemk34  40912  cdlemk39  40918  cdlemkyyN  40964
  Copyright terms: Public domain W3C validator