![]() |
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 1892: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2177, sps 2202 and eximd 2232, 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 148 | . . . 4 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
3 | 2 | al2imi 1892 | . . 3 ⊢ (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓)) |
4 | alnex 1855 | . . 3 ⊢ (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒) | |
5 | alnex 1855 | . . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓) | |
6 | 3, 4, 5 | 3imtr3g 284 | . 2 ⊢ (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓)) |
7 | 6 | con4d 114 | 1 ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1630 ∃wex 1853 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 |
This theorem depends on definitions: df-bi 197 df-ex 1854 |
This theorem is referenced by: alexbii 1909 exim 1910 exanOLD 1938 eximdh 1940 19.29 1950 19.29r 1951 19.35 1954 19.25 1957 19.30 1958 19.40b 1964 speimfw 2042 aeveq 2133 2ax6elem 2586 mo3 2645 mopick 2673 2mo 2689 ssopab2 5151 ssoprab2 6876 axextnd 9605 bj-2exim 32901 bj-exalimi 32918 bj-sb56 32945 wl-dveeq12 33624 wl-mo3t 33671 pm10.56 39071 2exim 39080 |
Copyright terms: Public domain | W3C validator |