![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > reximi | GIF version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.) |
Ref | Expression |
---|---|
reximi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
reximi | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximi.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | a1i 9 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
3 | 2 | reximia 2499 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1461 ∃wrex 2389 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-4 1468 ax-ial 1495 |
This theorem depends on definitions: df-bi 116 df-ral 2393 df-rex 2394 |
This theorem is referenced by: r19.29d2r 2548 r19.35-1 2553 r19.40 2557 reu3 2841 ssiun 3819 iinss 3828 elunirn 5619 tfrcllemssrecs 6200 nnawordex 6375 iinerm 6452 erovlem 6472 xpf1o 6688 fidcenumlemim 6789 genprndl 7270 genprndu 7271 appdiv0nq 7313 ltexprlemm 7349 recexsrlem 7510 rereceu 7617 recexre 8251 rexanre 10877 climi2 10942 climi0 10943 climcaucn 11005 gcdsupex 11487 gcdsupcl 11488 bezoutlemeu 11534 dfgcd3 11537 eltg2b 12059 lmcvg 12221 cnptoprest 12243 lmtopcnp 12254 txbas 12262 metrest 12488 bj-findis 12856 |
Copyright terms: Public domain | W3C validator |