![]() |
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 3146 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
3 | rexim 3203 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2079 ∀wral 3103 ∃wrex 3104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1760 df-ral 3108 df-rex 3109 |
This theorem is referenced by: reximdv 3233 reximdva 3234 reuind 3673 wefrc 5429 isomin 6944 isofrlem 6947 onfununi 7821 oaordex 8025 odi 8046 omass 8047 omeulem1 8049 noinfep 8958 rankwflemb 9057 infxpenlem 9274 coflim 9518 coftr 9530 zorn2lem7 9759 suplem1pr 10309 axpre-sup 10426 climbdd 14850 filufint 22200 cvati 29822 atcvat4i 29853 mdsymlem2 29860 mdsymlem3 29861 sumdmdii 29871 iccllysconn 32061 dftrpred3g 32626 incsequz2 34502 lcvat 35647 hlrelat3 36029 cvrval3 36030 cvrval4N 36031 2atlt 36056 cvrat4 36060 atbtwnexOLDN 36064 atbtwnex 36065 athgt 36073 2llnmat 36141 lnjatN 36397 2lnat 36401 cdlemb 36411 lhpexle3lem 36628 cdlemf1 37178 cdlemf2 37179 cdlemf 37180 cdlemk26b-3 37522 dvh4dimlem 38060 upbdrech 41066 limcperiod 41405 cncfshift 41652 cncfperiod 41657 |
Copyright terms: Public domain | W3C validator |