![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > aleximi | Structured version Visualization version GIF version |
Description: A variant of al2imi 1810: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2141, sps 2171 and eximd 2202, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.) |
Ref | Expression |
---|---|
aleximi.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
aleximi | ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aleximi.1 | . . . . 5 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | con3d 152 | . . . 4 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
3 | 2 | al2imi 1810 | . . 3 ⊢ (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓)) |
4 | alnex 1776 | . . 3 ⊢ (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒) | |
5 | alnex 1776 | . . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓) | |
6 | 3, 4, 5 | 3imtr3g 295 | . 2 ⊢ (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓)) |
7 | 6 | con4d 115 | 1 ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1532 ∃wex 1774 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 206 df-ex 1775 |
This theorem is referenced by: alexbii 1828 exim 1829 eximdh 1860 19.29 1869 19.29r 1870 19.35 1873 19.25 1876 19.30 1877 19.40b 1884 exintr 1888 19.36imv 1941 speimfw 1960 aeveq 2052 sbequ2 2234 2ax6elem 2464 sb1 2472 dfeumo 2526 mo3 2553 mo4 2555 mopick 2616 2mo 2639 ssel 3971 ssopab2 5542 ssoprab2 7482 axextnd 10606 bj-2exim 36024 bj-exalimi 36045 bj-cbvalimt 36051 bj-eximcom 36055 bj-subst 36073 bj-gabss 36349 wl-mo3t 36978 pm10.56 43730 2exim 43739 |
Copyright terms: Public domain | W3C validator |