| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > reximdvai | Structured version Visualization version GIF version | ||
| Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
| Ref | Expression |
|---|---|
| reximdvai.1 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
| Ref | Expression |
|---|---|
| reximdvai | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reximdvai.1 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) | |
| 2 | 1 | imdistand 570 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐴 ∧ 𝜒))) |
| 3 | 2 | reximdv2 3164 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ∃wrex 3070 |
| 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-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: reximdva 3168 reximdv 3170 reuind 3759 wefrc 5679 isomin 7357 isofrlem 7360 onfununi 8381 oaordex 8596 odi 8617 omass 8618 omeulem1 8620 noinfep 9700 rankwflemb 9833 infxpenlem 10053 coflim 10301 coftr 10313 zorn2lem7 10542 suplem1pr 11092 axpre-sup 11209 climbdd 15708 filufint 23928 cvati 32385 atcvat4i 32416 mdsymlem2 32423 mdsymlem3 32424 sumdmdii 32434 iccllysconn 35255 incsequz2 37756 lcvat 39031 hlrelat3 39414 cvrval3 39415 cvrval4N 39416 2atlt 39441 cvrat4 39445 atbtwnexOLDN 39449 atbtwnex 39450 athgt 39458 2llnmat 39526 lnjatN 39782 2lnat 39786 cdlemb 39796 lhpexle3lem 40013 cdlemf1 40563 cdlemf2 40564 cdlemf 40565 cdlemk26b-3 40907 dvh4dimlem 41445 cantnf2 43338 relpfrlem 44974 upbdrech 45317 limcperiod 45643 cncfshift 45889 cncfperiod 45894 |
| Copyright terms: Public domain | W3C validator |