![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > alimi | Unicode version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
alimi.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
alimi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1333 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | alimi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpg 1337 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 7 ax-5 1333 ax-gen 1335 |
This theorem is referenced by: 2alimi 1342 al2imi 1344 alrimih 1355 hbal 1363 19.26 1367 19.33 1370 hbequid 1403 equidqe 1422 hbim 1434 hbor 1435 nford 1456 nfand 1457 nfalt 1467 19.21ht 1470 exbi 1492 19.29 1508 19.25 1514 alexim 1533 alexnim 1536 19.9hd 1549 19.32r 1567 ax10 1602 spimh 1622 equvini 1638 nfexd 1641 stdpc4 1655 ax10oe 1675 sbcof2 1688 sb4bor 1713 nfsb2or 1715 spsbim 1721 ax16i 1735 sbi2v 1769 nfsbt 1847 nfsbd 1848 sbalyz 1872 hbsb4t 1886 dvelimor 1891 sbal2 1895 mo2n 1925 eumo0 1928 mor 1939 bm1.1 2022 alral 2361 rgen2a 2369 ralimi2 2375 rexim 2407 r19.32r 2451 ceqsalt 2574 spcgft 2624 spcegft 2626 spc2gv 2637 spc3gv 2639 rspct 2643 elabgt 2678 reu6 2724 sbciegft 2787 csbnestgf 2892 rabss2 3017 rabxmdc 3243 undif4 3278 ssdif0im 3280 inssdif0im 3285 ssundifim 3300 ralf0 3318 ralm 3319 intmin4 3634 dfiin2g 3681 invdisj 3750 trint 3860 a9evsep 3870 axnul 3873 csbexga 3876 ordunisuc2r 4205 tfi 4248 peano5 4264 ssrelrel 4383 issref 4650 iotanul 4825 iota4 4828 dffun5r 4857 fv3 5140 mptfvex 5199 ssoprab2 5503 mpt2fvex 5771 bj-nfalt 9239 elabgft1 9252 bj-rspgt 9260 bj-axemptylem 9347 bj-indind 9391 peano5setOLD 9400 setindis 9427 bdsetindis 9429 bj-inf2vnlem1 9430 bj-inf2vn 9434 bj-inf2vn2 9435 |
Copyright terms: Public domain | W3C validator |