![]() |
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 1198 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2ant3 1132 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: totprob 34198 cdleme19b 39927 cdleme19d 39929 cdleme19e 39930 cdleme20h 39939 cdleme20l2 39944 cdleme20m 39946 cdleme21d 39953 cdleme21e 39954 cdleme22e 39967 cdleme22f2 39970 cdleme22g 39971 cdleme26e 39982 cdleme28a 39993 cdleme28b 39994 cdleme37m 40085 cdleme39n 40089 cdlemeg46gfre 40155 cdlemg28a 40316 cdlemg28b 40326 cdlemk3 40456 cdlemk5a 40458 cdlemk6 40460 cdlemkuat 40489 cdlemkid2 40547 |
Copyright terms: Public domain | W3C validator |