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 2565 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 ∃wrex 2449 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-ial 1527 |
This theorem depends on definitions: df-bi 116 df-ral 2453 df-rex 2454 |
This theorem is referenced by: r19.29d2r 2614 r19.35-1 2620 r19.40 2624 reu3 2920 ssiun 3913 iinss 3922 elunirn 5742 tfrcllemssrecs 6328 nnawordex 6504 iinerm 6581 erovlem 6601 xpf1o 6818 fidcenumlemim 6925 omniwomnimkv 7139 genprndl 7470 genprndu 7471 appdiv0nq 7513 ltexprlemm 7549 recexsrlem 7723 rereceu 7838 recexre 8484 aprcl 8552 rexanre 11171 climi2 11238 climi0 11239 climcaucn 11301 prodmodclem2 11527 prodmodc 11528 gcdsupex 11899 gcdsupcl 11900 bezoutlemeu 11949 dfgcd3 11952 isnsgrp 12634 eltg2b 12807 lmcvg 12970 cnptoprest 12992 lmtopcnp 13003 txbas 13011 metrest 13259 2sqlem7 13710 bj-charfunbi 13806 bj-findis 13974 |
Copyright terms: Public domain | W3C validator |