![]() |
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 2467 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-gen 1408 |
This theorem depends on definitions: df-bi 116 df-ral 2395 |
This theorem is referenced by: 2ralimi 2470 ral2imi 2471 r19.26 2532 r19.29 2543 rr19.3v 2793 rr19.28v 2794 reu3 2843 uniiunlem 3151 reupick2 3328 uniss2 3733 ss2iun 3794 iineq2 3796 iunss2 3824 disjss2 3875 disjeq2 3876 disjnim 3886 repizf 4004 abnexg 4327 reusv3i 4340 tfis 4457 ssrel2 4589 issref 4879 dmmptg 4994 funco 5121 fununi 5149 fun11uni 5151 funimaexglem 5164 fnmpt 5207 fun11iun 5344 mpteqb 5465 chfnrn 5485 dffo5 5523 ffvresb 5537 fmptcof 5541 dfmptg 5553 mpo2eqb 5834 ralrnmpo 5839 rexrnmpo 5840 fnmpo 6054 mpoexxg 6062 smores 6143 riinerm 6456 ixpm 6578 difinfinf 6938 cauappcvgprlemdisj 7407 caucvgsrlemasr 7532 caucvgsr 7544 rexuz3 10654 recvguniq 10659 cau3lem 10778 caubnd2 10781 rexanre 10884 climi2 10949 climi0 10950 climcaucn 11012 ndvdssub 11475 gcdsupex 11494 gcdsupcl 11495 bezoutlemmo 11540 eltg2b 12066 neipsm 12166 lmcvg 12228 txlm 12290 metrest 12495 mulcncflem 12576 bj-indint 12819 bj-indind 12820 bj-bdfindis 12835 setindis 12855 bdsetindis 12857 |
Copyright terms: Public domain | W3C validator |