![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp22r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp22r | ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2r 1197 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant2 1131 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ 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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: frrlem10 8301 ttrclselem2 9751 ax5seglem6 28817 segconeu 35735 3atlem2 39084 lplnexllnN 39164 lplncvrlvol2 39215 4atex 39676 cdleme3g 39834 cdleme3h 39835 cdleme11h 39866 cdleme20bN 39910 cdleme20c 39911 cdleme20f 39914 cdleme20g 39915 cdleme20j 39918 cdleme20l2 39921 cdleme20l 39922 cdleme21ct 39929 cdleme26e 39959 cdleme43fsv1snlem 40020 cdleme39n 40066 cdleme40m 40067 cdleme42k 40084 cdlemg6c 40220 cdlemg31d 40300 cdlemg33a 40306 cdlemg33c 40308 cdlemg33d 40309 cdlemg33e 40310 cdlemg33 40311 cdlemh 40417 cdlemk7u-2N 40488 cdlemk11u-2N 40489 cdlemk12u-2N 40490 cdlemk20-2N 40492 cdlemk28-3 40508 cdlemk33N 40509 cdlemk34 40510 cdlemk39 40516 cdlemkyyN 40562 |
Copyright terms: Public domain | W3C validator |