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 2456 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1433 ∃wrex 2349 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-ial 1467 |
This theorem depends on definitions: df-bi 115 df-ral 2353 df-rex 2354 |
This theorem is referenced by: r19.29d2r 2499 r19.35-1 2504 r19.40 2508 reu3 2782 ssiun 3720 iinss 3729 elunirn 5426 nnawordex 6124 iinerm 6201 erovlem 6221 genprndl 6711 genprndu 6712 appdiv0nq 6754 ltexprlemm 6790 recexsrlem 6951 rereceu 7055 recexre 7678 rexanre 10106 climi2 10127 climi0 10128 climcaucn 10188 gcdsupex 10349 gcdsupcl 10350 bezoutlemeu 10396 dfgcd3 10399 bj-findis 10774 |
Copyright terms: Public domain | W3C validator |