![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE 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 | ⊢ (∃x∃yφ → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimivv.1 | . . 3 ⊢ (φ → ψ) | |
2 | 1 | exlimiv 1634 | . 2 ⊢ (∃yφ → ψ) |
3 | 2 | exlimiv 1634 | 1 ⊢ (∃x∃yφ → ψ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1541 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 |
This theorem depends on definitions: df-bi 177 df-ex 1542 |
This theorem is referenced by: 2mo 2282 cgsex2g 2891 cgsex4g 2892 elxpk 4196 opkabssvvk 4208 sikss1c1c 4267 ins2kss 4279 ins3kss 4280 cokrelk 4284 pw1equn 4331 pw1eqadj 4332 copsexg 4607 elopab 4696 brsi 4761 optocl 4838 xpnz 5045 dfco2a 5081 dfxp2 5113 1stfo 5505 2ndfo 5506 brswap 5509 oprabid 5550 brtxp 5783 txpcofun 5803 pw1fnf1o 5855 entr 6038 unen 6048 xpen 6055 xpassen 6057 mucnc 6131 muccl 6132 muccom 6134 mucass 6135 ncaddccl 6144 ncdisjeq 6148 tcdi 6164 elce 6175 ce0addcnnul 6179 cenc 6181 sbthlem3 6205 dflec3 6221 nclenc 6222 lenc 6223 tc11 6228 taddc 6229 letc 6231 ce2le 6233 muc0or 6252 frecxp 6314 |
Copyright terms: Public domain | W3C validator |