![]() |
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 1200 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2ant3 1134 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 207 df-an 396 df-3an 1088 |
This theorem is referenced by: totprob 34409 cdleme19b 40287 cdleme19d 40289 cdleme19e 40290 cdleme20h 40299 cdleme20l2 40304 cdleme20m 40306 cdleme21d 40313 cdleme21e 40314 cdleme22e 40327 cdleme22f2 40330 cdleme22g 40331 cdleme26e 40342 cdleme28a 40353 cdleme28b 40354 cdleme37m 40445 cdleme39n 40449 cdlemeg46gfre 40515 cdlemg28a 40676 cdlemg28b 40686 cdlemk3 40816 cdlemk5a 40818 cdlemk6 40820 cdlemkuat 40849 cdlemkid2 40907 |
Copyright terms: Public domain | W3C validator |