Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp33r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp33r | ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3r 1194 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant3 1127 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: totprob 31584 cdleme19b 37320 cdleme19e 37323 cdleme20h 37332 cdleme20l2 37337 cdleme20m 37339 cdleme21d 37346 cdleme21e 37347 cdleme22eALTN 37361 cdleme22f2 37363 cdleme22g 37364 cdleme26e 37375 cdleme37m 37478 cdlemeg46gfre 37548 cdlemg28a 37709 cdlemg28b 37719 cdlemk5a 37851 cdlemk6 37853 |
Copyright terms: Public domain | W3C validator |