![]() |
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 2572 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 ∃wrex 2456 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 df-ral 2460 df-rex 2461 |
This theorem is referenced by: r19.29d2r 2621 r19.35-1 2627 r19.40 2631 reu3 2929 ssiun 3930 iinss 3940 elunirn 5769 tfrcllemssrecs 6355 nnawordex 6532 iinerm 6609 erovlem 6629 xpf1o 6846 fidcenumlemim 6953 omniwomnimkv 7167 genprndl 7522 genprndu 7523 appdiv0nq 7565 ltexprlemm 7601 recexsrlem 7775 rereceu 7890 recexre 8537 aprcl 8605 rexanre 11231 climi2 11298 climi0 11299 climcaucn 11361 prodmodclem2 11587 prodmodc 11588 gcdsupex 11960 gcdsupcl 11961 bezoutlemeu 12010 dfgcd3 12013 isnsgrp 12817 eltg2b 13639 lmcvg 13802 cnptoprest 13824 lmtopcnp 13835 txbas 13843 metrest 14091 2sqlem7 14553 bj-charfunbi 14648 bj-findis 14816 |
Copyright terms: Public domain | W3C validator |