Description: Abbreviated version of axc7 using the existential quantifier. Corresponds to the dual of Axiom (B) of modal logic. (Contributed by NM, 5-Aug-1993) (Proof shortened by Wolf Lammen, 8-Jul-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axc7e | |- ( E. x A. x ph -> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hbe1a | |- ( E. x A. x ph -> A. x ph ) |
|
| 2 | 1 | 19.21bi | |- ( E. x A. x ph -> ph ) |