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.) |
Ref | Expression |
---|---|
reximdvai.1 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
Ref | Expression |
---|---|
reximdvai | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdvai.1 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) | |
2 | 1 | ralrimiv 2948 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
3 | rexim 2991 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-ral 2901 df-rex 2902 |
This theorem is referenced by: reximdv 2999 reximdva 3000 reuind 3378 wefrc 5032 isomin 6487 isofrlem 6490 onfununi 7325 oaordex 7525 odi 7546 omass 7547 omeulem1 7549 noinfep 8440 rankwflemb 8539 infxpenlem 8719 coflim 8966 coftr 8978 zorn2lem7 9207 suplem1pr 9753 axpre-sup 9869 climbdd 14250 filufint 21534 cvati 28609 atcvat4i 28640 mdsymlem2 28647 mdsymlem3 28648 sumdmdii 28658 iccllyscon 30486 dftrpred3g 30977 incsequz2 32715 lcvat 33335 hlrelat3 33716 cvrval3 33717 cvrval4N 33718 2atlt 33743 cvrat4 33747 atbtwnexOLDN 33751 atbtwnex 33752 athgt 33760 2llnmat 33828 lnjatN 34084 2lnat 34088 cdlemb 34098 lhpexle3lem 34315 cdlemf1 34867 cdlemf2 34868 cdlemf 34869 cdlemk26b-3 35211 dvh4dimlem 35750 upbdrech 38460 limcperiod 38695 cncfshift 38759 cncfperiod 38764 |
Copyright terms: Public domain | W3C validator |