Description: Existential quantification of a conjunction expressed with only primitive symbols ( -> , -. , A. ). (Contributed by NM, 10-May-1993) State the most general instance. (Revised by BJ, 29-Sep-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | exnalimn | |- ( E. x ( ph /\ ps ) <-> -. A. x ( ph -> -. ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alinexa | |- ( A. x ( ph -> -. ps ) <-> -. E. x ( ph /\ ps ) ) |
|
| 2 | 1 | con2bii | |- ( E. x ( ph /\ ps ) <-> -. A. x ( ph -> -. ps ) ) |