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 1082 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2ant3 1077 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: totprob 29816 cdleme19b 34610 cdleme19d 34612 cdleme19e 34613 cdleme20h 34622 cdleme20l2 34627 cdleme20m 34629 cdleme21d 34636 cdleme21e 34637 cdleme22e 34650 cdleme22f2 34653 cdleme22g 34654 cdleme26e 34665 cdleme28a 34676 cdleme28b 34677 cdleme37m 34768 cdleme39n 34772 cdlemeg46gfre 34838 cdlemg28a 34999 cdlemg28b 35009 cdlemk3 35139 cdlemk5a 35141 cdlemk6 35143 cdlemkuat 35172 cdlemkid2 35230 |
Copyright terms: Public domain | W3C validator |