![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exlimivv | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.) |
Ref | Expression |
---|---|
exlimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
exlimivv | ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | exlimiv 1535 | . 2 ⊢ (∃𝑦𝜑 → 𝜓) |
3 | 2 | exlimiv 1535 | 1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1427 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-gen 1384 ax-ie2 1429 ax-17 1465 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: cgsex2g 2656 cgsex4g 2657 opabss 3908 copsexg 4080 elopab 4094 epelg 4126 0nelelxp 4480 elvvuni 4515 optocl 4527 xpsspw 4563 relopabi 4576 relop 4599 elreldm 4674 xpmlem 4865 dfco2a 4944 unielrel 4971 oprabid 5695 1stval2 5940 2ndval2 5941 xp1st 5950 xp2nd 5951 poxp 6011 rntpos 6036 dftpos4 6042 tpostpos 6043 tfrlem7 6096 th3qlem2 6409 ener 6550 domtr 6556 unen 6587 xpsnen 6591 mapen 6616 ltdcnq 7017 archnqq 7037 enq0tr 7054 nqnq0pi 7058 nqnq0 7061 nqpnq0nq 7073 nqnq0a 7074 nqnq0m 7075 nq0m0r 7076 nq0a0 7077 nq02m 7085 prarloc 7123 axaddcl 7462 axmulcl 7464 hashfacen 10302 bj-inex 12071 |
Copyright terms: Public domain | W3C validator |