![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp32r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp32r | ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2r 1191 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant3 1126 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1078 |
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 208 df-an 397 df-3an 1080 |
This theorem is referenced by: cdlema1N 36408 paddasslem15 36451 4atex2-0aOLDN 36695 4atex3 36698 cdleme19b 36921 cdleme19d 36923 cdleme19e 36924 cdleme20d 36929 cdleme20f 36931 cdleme20g 36932 cdleme21d 36947 cdleme21e 36948 cdleme22cN 36959 cdleme22e 36961 cdleme22f2 36964 cdleme26e 36976 cdleme28a 36987 cdleme37m 37079 cdlemg28b 37320 cdlemk3 37450 cdlemk12 37467 cdlemk12u 37489 cdlemkoatnle-2N 37492 cdlemk13-2N 37493 cdlemkole-2N 37494 cdlemk14-2N 37495 cdlemk15-2N 37496 cdlemk16-2N 37497 cdlemk17-2N 37498 cdlemk18-2N 37503 cdlemk19-2N 37504 cdlemk7u-2N 37505 cdlemk11u-2N 37506 cdlemk20-2N 37509 cdlemk30 37511 cdlemk23-3 37519 cdlemk24-3 37520 |
Copyright terms: Public domain | W3C validator |