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 1204 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant3 1137 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: totprob 32106 cdleme19b 38055 cdleme19e 38058 cdleme20h 38067 cdleme20l2 38072 cdleme20m 38074 cdleme21d 38081 cdleme21e 38082 cdleme22eALTN 38096 cdleme22f2 38098 cdleme22g 38099 cdleme26e 38110 cdleme37m 38213 cdlemeg46gfre 38283 cdlemg28a 38444 cdlemg28b 38454 cdlemk5a 38586 cdlemk6 38588 |
Copyright terms: Public domain | W3C validator |