**Description:** Inference associated with 19.23 . See exlimiv for a version with a
disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993) (Revised by Mario Carneiro, 24-Sep-2016)

Ref | Expression | ||
---|---|---|---|

Hypotheses | exlimi.1 | $${\u22a2}\u2132{x}\phantom{\rule{.4em}{0ex}}{\psi}$$ | |

exlimi.2 | $${\u22a2}{\phi}\to {\psi}$$ | ||

Assertion | exlimi | $${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to {\psi}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | exlimi.1 | $${\u22a2}\u2132{x}\phantom{\rule{.4em}{0ex}}{\psi}$$ | |

2 | exlimi.2 | $${\u22a2}{\phi}\to {\psi}$$ | |

3 | 1 | 19.23 | $${\u22a2}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi}\to {\psi}\right)\leftrightarrow \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to {\psi}\right)$$ |

4 | 3 2 | mpgbi | $${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to {\psi}$$ |