![]() |
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 569 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐴 ∧ 𝜒))) |
3 | 2 | reximdv2 3153 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 ∃wrex 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-rex 3060 |
This theorem is referenced by: reximdva 3157 reximdv 3159 reuind 3745 wefrc 5672 isomin 7344 isofrlem 7347 onfununi 8362 oaordex 8579 odi 8600 omass 8601 omeulem1 8603 noinfep 9685 rankwflemb 9818 infxpenlem 10038 coflim 10286 coftr 10298 zorn2lem7 10527 suplem1pr 11077 axpre-sup 11194 climbdd 15654 filufint 23868 cvati 32248 atcvat4i 32279 mdsymlem2 32286 mdsymlem3 32287 sumdmdii 32297 iccllysconn 34991 incsequz2 37353 lcvat 38632 hlrelat3 39015 cvrval3 39016 cvrval4N 39017 2atlt 39042 cvrat4 39046 atbtwnexOLDN 39050 atbtwnex 39051 athgt 39059 2llnmat 39127 lnjatN 39383 2lnat 39387 cdlemb 39397 lhpexle3lem 39614 cdlemf1 40164 cdlemf2 40165 cdlemf 40166 cdlemk26b-3 40508 dvh4dimlem 41046 cantnf2 42896 upbdrech 44825 limcperiod 45154 cncfshift 45400 cncfperiod 45405 |
Copyright terms: Public domain | W3C validator |