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 1823: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2153, sps 2183 and eximd 2215, 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 155 | . . . 4 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
3 | 2 | al2imi 1823 | . . 3 ⊢ (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓)) |
4 | alnex 1789 | . . 3 ⊢ (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒) | |
5 | alnex 1789 | . . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓) | |
6 | 3, 4, 5 | 3imtr3g 298 | . 2 ⊢ (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓)) |
7 | 6 | con4d 115 | 1 ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1541 ∃wex 1787 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-ex 1788 |
This theorem is referenced by: alexbii 1840 exim 1841 eximdh 1872 19.29 1881 19.29r 1882 19.35 1885 19.25 1888 19.30 1889 19.40b 1896 exintr 1900 19.36imv 1953 speimfw 1972 aeveq 2063 sbequ2 2247 2ax6elem 2470 sb1 2479 dfeumo 2537 mo3 2564 mo4 2566 mopick 2627 2mo 2650 ssel 3907 ssopab2 5441 ssoprab2 7297 axextnd 10229 bj-2exim 34556 bj-exalimi 34577 bj-cbvalimt 34583 bj-eximcom 34587 bj-subst 34605 bj-gabss 34886 wl-mo3t 35494 pm10.56 41689 2exim 41698 |
Copyright terms: Public domain | W3C validator |