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 2493 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 wral 2416 |
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 1423 ax-gen 1425 |
This theorem depends on definitions: df-bi 116 df-ral 2421 |
This theorem is referenced by: 2ralimi 2496 ral2imi 2497 r19.26 2558 r19.29 2569 rr19.3v 2823 rr19.28v 2824 reu3 2874 uniiunlem 3185 reupick2 3362 uniss2 3767 ss2iun 3828 iineq2 3830 iunss2 3858 disjss2 3909 disjeq2 3910 disjnim 3920 repizf 4044 abnexg 4367 reusv3i 4380 tfis 4497 ssrel2 4629 issref 4921 dmmptg 5036 funco 5163 fununi 5191 fun11uni 5193 funimaexglem 5206 fnmpt 5249 fun11iun 5388 mpteqb 5511 chfnrn 5531 dffo5 5569 ffvresb 5583 fmptcof 5587 dfmptg 5599 mpo2eqb 5880 ralrnmpo 5885 rexrnmpo 5886 fnmpo 6100 mpoexxg 6108 smores 6189 riinerm 6502 ixpm 6624 difinfinf 6986 cauappcvgprlemdisj 7459 caucvgsrlemasr 7598 caucvgsr 7610 suplocsr 7617 rexuz3 10762 recvguniq 10767 cau3lem 10886 caubnd2 10889 rexanre 10992 climi2 11057 climi0 11058 climcaucn 11120 ndvdssub 11627 gcdsupex 11646 gcdsupcl 11647 bezoutlemmo 11694 eltg2b 12223 neipsm 12323 lmcvg 12386 txlm 12448 metrest 12675 mulcncflem 12759 bj-indint 13129 bj-indind 13130 bj-bdfindis 13145 setindis 13165 bdsetindis 13167 |
Copyright terms: Public domain | W3C validator |