![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp33l | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp33l | ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3l 1259 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2ant3 1166 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 ∧ w3a 1108 |
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 386 df-3an 1110 |
This theorem is referenced by: totprob 30998 cdleme19b 36317 cdleme19d 36319 cdleme19e 36320 cdleme20h 36329 cdleme20l2 36334 cdleme20m 36336 cdleme21d 36343 cdleme21e 36344 cdleme22e 36357 cdleme22f2 36360 cdleme22g 36361 cdleme26e 36372 cdleme28a 36383 cdleme28b 36384 cdleme37m 36475 cdleme39n 36479 cdlemeg46gfre 36545 cdlemg28a 36706 cdlemg28b 36716 cdlemk3 36846 cdlemk5a 36848 cdlemk6 36850 cdlemkuat 36879 cdlemkid2 36937 |
Copyright terms: Public domain | W3C validator |