![]() |
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 1240 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant2 1128 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 197 df-an 385 df-3an 1074 |
This theorem is referenced by: ax5seglem6 26005 segconeu 32416 3atlem2 35265 lplnexllnN 35345 lplncvrlvol2 35396 4atex 35857 cdleme3g 36016 cdleme3h 36017 cdleme11h 36048 cdleme20bN 36092 cdleme20c 36093 cdleme20f 36096 cdleme20g 36097 cdleme20j 36100 cdleme20l2 36103 cdleme20l 36104 cdleme21ct 36111 cdleme26e 36141 cdleme43fsv1snlem 36202 cdleme39n 36248 cdleme40m 36249 cdleme42k 36266 cdlemg6c 36402 cdlemg31d 36482 cdlemg33a 36488 cdlemg33c 36490 cdlemg33d 36491 cdlemg33e 36492 cdlemg33 36493 cdlemh 36599 cdlemk7u-2N 36670 cdlemk11u-2N 36671 cdlemk12u-2N 36672 cdlemk20-2N 36674 cdlemk28-3 36690 cdlemk33N 36691 cdlemk34 36692 cdlemk39 36698 cdlemkyyN 36744 |
Copyright terms: Public domain | W3C validator |