![]() |
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 1180 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant2 1114 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 |
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 199 df-an 388 df-3an 1070 |
This theorem is referenced by: ax5seglem6 26423 frrlem10 32659 segconeu 32999 3atlem2 36071 lplnexllnN 36151 lplncvrlvol2 36202 4atex 36663 cdleme3g 36821 cdleme3h 36822 cdleme11h 36853 cdleme20bN 36897 cdleme20c 36898 cdleme20f 36901 cdleme20g 36902 cdleme20j 36905 cdleme20l2 36908 cdleme20l 36909 cdleme21ct 36916 cdleme26e 36946 cdleme43fsv1snlem 37007 cdleme39n 37053 cdleme40m 37054 cdleme42k 37071 cdlemg6c 37207 cdlemg31d 37287 cdlemg33a 37293 cdlemg33c 37295 cdlemg33d 37296 cdlemg33e 37297 cdlemg33 37298 cdlemh 37404 cdlemk7u-2N 37475 cdlemk11u-2N 37476 cdlemk12u-2N 37477 cdlemk20-2N 37479 cdlemk28-3 37495 cdlemk33N 37496 cdlemk34 37497 cdlemk39 37503 cdlemkyyN 37549 |
Copyright terms: Public domain | W3C validator |