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 3104 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
3 | rexim 3163 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 ∀wral 3061 ∃wrex 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-ral 3066 df-rex 3067 |
This theorem is referenced by: reximdv 3192 reximdva 3193 reuind 3666 wefrc 5545 isomin 7146 isofrlem 7149 onfununi 8078 oaordex 8286 odi 8307 omass 8308 omeulem1 8310 noinfep 9275 dftrpred3g 9339 rankwflemb 9409 infxpenlem 9627 coflim 9875 coftr 9887 zorn2lem7 10116 suplem1pr 10666 axpre-sup 10783 climbdd 15235 filufint 22817 cvati 30447 atcvat4i 30478 mdsymlem2 30485 mdsymlem3 30486 sumdmdii 30496 iccllysconn 32925 incsequz2 35644 lcvat 36781 hlrelat3 37163 cvrval3 37164 cvrval4N 37165 2atlt 37190 cvrat4 37194 atbtwnexOLDN 37198 atbtwnex 37199 athgt 37207 2llnmat 37275 lnjatN 37531 2lnat 37535 cdlemb 37545 lhpexle3lem 37762 cdlemf1 38312 cdlemf2 38313 cdlemf 38314 cdlemk26b-3 38656 dvh4dimlem 39194 upbdrech 42517 limcperiod 42844 cncfshift 43090 cncfperiod 43095 |
Copyright terms: Public domain | W3C validator |