diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index b383aed63c4ad5110d6c13660f74e64f996ade26..b1a84922bdbba41452f6f70cbca9c4e96f01b713 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -328,6 +328,9 @@ _introduction patterns_:
   + Either the proposition `P` or `Q` should be persistent.
   + Either `ipat1` or `ipat2` should be `_`, which results in one of the
     conjuncts to be thrown away.
+- `[% ipat]` : existential elimination. Falls back to (separating) conjunction
+  elimination in case the hypothesis is not an existential, so this pattern also
+  works for (separating) conjunctions with a pure left-hand side.
 - `(pat1 & pat2 & ... & patn)` : syntactic sugar for `[pat1 [pat2 .. patn ..]]`
   to destruct nested (separating) conjunctions.
 - `[ipat1|ipat2]` : disjunction elimination.