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 3915 iinss 3924 elunirn 5745 tfrcllemssrecs 6331 nnawordex 6508 iinerm 6585 erovlem 6605 xpf1o 6822 fidcenumlemim 6929 omniwomnimkv 7143 genprndl 7483 genprndu 7484 appdiv0nq 7526 ltexprlemm 7562 recexsrlem 7736 rereceu 7851 recexre 8497 aprcl 8565 rexanre 11184 climi2 11251 climi0 11252 climcaucn 11314 prodmodclem2 11540 prodmodc 11541 gcdsupex 11912 gcdsupcl 11913 bezoutlemeu 11962 dfgcd3 11965 isnsgrp 12647 eltg2b 12848 lmcvg 13011 cnptoprest 13033 lmtopcnp 13044 txbas 13052 metrest 13300 2sqlem7 13751 bj-charfunbi 13846 bj-findis 14014 |
Copyright terms: Public domain | W3C validator |