![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralimi | Unicode version |
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
ralimi.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralimi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimi.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ralimia 2551 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 1458 ax-gen 1460 |
This theorem depends on definitions: df-bi 117 df-ral 2473 |
This theorem is referenced by: 2ralimi 2554 ral2imi 2555 r19.26 2616 r19.29 2627 rr19.3v 2891 rr19.28v 2892 reu3 2942 uniiunlem 3259 reupick2 3436 uniss2 3855 ss2iun 3916 iineq2 3918 iunss2 3946 disjss2 3998 disjeq2 3999 disjnim 4009 repizf 4134 abnexg 4464 reusv3i 4477 tfis 4600 ssrel2 4734 issref 5029 dmmptg 5144 funco 5275 fununi 5303 fun11uni 5305 funimaexglem 5318 fnmpt 5361 fun11iun 5501 mpteqb 5626 chfnrn 5647 dffo5 5685 ffvresb 5699 fmptcof 5703 dfmptg 5715 mpo2eqb 6005 ralrnmpo 6010 rexrnmpo 6011 fnmpo 6226 mpoexxg 6234 smores 6316 riinerm 6633 ixpm 6755 difinfinf 7129 nninfwlpoimlemginf 7203 exmidontriimlem1 7249 onntri13 7266 onntri24 7270 cc4f 7297 cc4n 7299 cauappcvgprlemdisj 7679 caucvgsrlemasr 7818 caucvgsr 7830 suplocsr 7837 rexuz3 11030 recvguniq 11035 cau3lem 11154 caubnd2 11157 rexanre 11260 climi2 11327 climi0 11328 climcaucn 11390 ndvdssub 11966 gcdsupex 11989 gcdsupcl 11990 bezoutlemmo 12038 ptex 12766 mgmidmo 12845 issubg2m 13125 eltg2b 14006 neipsm 14106 lmcvg 14169 txlm 14231 metrest 14458 mulcncflem 14542 bj-charfunbi 15016 bj-indint 15136 bj-indind 15137 bj-bdfindis 15152 setindis 15172 bdsetindis 15174 neap0mkv 15271 |
Copyright terms: Public domain | W3C validator |