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 1807: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2146, sps 2174 and eximd 2206, 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 1807 | . . 3 ⊢ (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓)) |
4 | alnex 1773 | . . 3 ⊢ (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒) | |
5 | alnex 1773 | . . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓) | |
6 | 3, 4, 5 | 3imtr3g 296 | . 2 ⊢ (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓)) |
7 | 6 | con4d 115 | 1 ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1526 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: alexbii 1824 exim 1825 eximdh 1856 19.29 1865 19.29r 1866 19.35 1869 19.25 1872 19.30 1873 19.40b 1880 exintr 1884 speimfw 1957 aeveq 2052 sbequ2 2240 2ax6elem 2485 sb1 2496 dfeumo 2612 mo3 2641 mo4 2643 mopick 2703 2mo 2726 ssopab2 5424 ssoprab2 7211 axextnd 10001 bj-2exim 33842 bj-exalimi 33863 bj-cbvalimt 33869 bj-eximcom 33873 bj-sb56 33891 wl-mo3t 34693 pm10.56 40579 2exim 40588 |
Copyright terms: Public domain | W3C validator |