![]() |
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 1243 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2ant3 1129 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1071 |
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 383 df-3an 1073 |
This theorem is referenced by: totprob 30829 cdleme19b 36113 cdleme19d 36115 cdleme19e 36116 cdleme20h 36125 cdleme20l2 36130 cdleme20m 36132 cdleme21d 36139 cdleme21e 36140 cdleme22e 36153 cdleme22f2 36156 cdleme22g 36157 cdleme26e 36168 cdleme28a 36179 cdleme28b 36180 cdleme37m 36271 cdleme39n 36275 cdlemeg46gfre 36341 cdlemg28a 36502 cdlemg28b 36512 cdlemk3 36642 cdlemk5a 36644 cdlemk6 36646 cdlemkuat 36675 cdlemkid2 36733 |
Copyright terms: Public domain | W3C validator |