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 2965 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
3 | rexim 3008 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-ral 2917 df-rex 2918 |
This theorem is referenced by: reximdv 3016 reximdva 3017 reuind 3411 wefrc 5108 isomin 6587 isofrlem 6590 onfununi 7438 oaordex 7638 odi 7659 omass 7660 omeulem1 7662 noinfep 8557 rankwflemb 8656 infxpenlem 8836 coflim 9083 coftr 9095 zorn2lem7 9324 suplem1pr 9874 axpre-sup 9990 climbdd 14402 filufint 21724 cvati 29225 atcvat4i 29256 mdsymlem2 29263 mdsymlem3 29264 sumdmdii 29274 iccllysconn 31232 dftrpred3g 31733 incsequz2 33545 lcvat 34317 hlrelat3 34698 cvrval3 34699 cvrval4N 34700 2atlt 34725 cvrat4 34729 atbtwnexOLDN 34733 atbtwnex 34734 athgt 34742 2llnmat 34810 lnjatN 35066 2lnat 35070 cdlemb 35080 lhpexle3lem 35297 cdlemf1 35849 cdlemf2 35850 cdlemf 35851 cdlemk26b-3 36193 dvh4dimlem 36732 upbdrech 39519 limcperiod 39860 cncfshift 40087 cncfperiod 40092 |
Copyright terms: Public domain | W3C validator |