|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 2eximdv | Structured version Visualization version GIF version | ||
| Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1834. (Contributed by NM, 3-Aug-1995.) | 
| Ref | Expression | 
|---|---|
| 2alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) | 
| Ref | Expression | 
|---|---|
| 2eximdv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 2alimdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | 1 | eximdv 1917 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒)) | 
| 3 | 2 | eximdv 1917 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∃wex 1779 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 | 
| This theorem depends on definitions: df-bi 207 df-ex 1780 | 
| This theorem is referenced by: 2eu6 2657 cgsex2g 3527 cgsex4g 3528 cgsex4gOLD 3529 spc2egv 3599 rexopabb 5533 relop 5861 elinxp 6037 opreuopreu 8059 en3 9316 en4 9317 addsrpr 11115 mulsrpr 11116 hash2prde 14509 hash3tpde 14532 pmtrrn2 19478 umgredg 29155 umgr2wlkon 29970 trsp2cyc 33143 acycgrsubgr 35163 satfvsucsuc 35370 fmla0xp 35388 fundmpss 35767 pellexlem5 42844 ax6e2eq 44577 fnchoice 45034 fzisoeu 45312 stoweidlem35 46050 stoweidlem60 46075 or2expropbi 47046 ich2exprop 47458 | 
| Copyright terms: Public domain | W3C validator |