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 1408 | . 2 | |
2 | alimi.1 | . 2 | |
3 | 1, 2 | mpg 1412 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1314 |
This theorem was proved from axioms: ax-mp 5 ax-5 1408 ax-gen 1410 |
This theorem is referenced by: 2alimi 1417 al2imi 1419 alrimih 1430 hbal 1438 19.26 1442 19.33 1445 hbequid 1478 equidqe 1497 hbim 1509 hbor 1510 nford 1531 nfand 1532 nfalt 1542 19.21ht 1545 exbi 1568 19.29 1584 19.25 1590 alexim 1609 alexnim 1612 19.9hd 1625 19.32r 1643 ax10 1680 spimh 1700 equvini 1716 nfexd 1719 stdpc4 1733 ax10oe 1753 sbcof2 1766 sb4bor 1791 nfsb2or 1793 spsbim 1799 ax16i 1814 sbi2v 1848 nfsbt 1927 nfsbd 1928 sbalyz 1952 hbsb4t 1966 dvelimor 1971 sbal2 1975 mo2n 2005 eumo0 2008 mor 2019 bm1.1 2102 alral 2455 rgen2a 2463 ralimi2 2469 rexim 2503 r19.32r 2555 ceqsalt 2686 spcgft 2737 spcegft 2739 spc2gv 2750 spc3gv 2752 rspct 2756 elabgt 2799 reu6 2846 sbciegft 2911 csbnestgf 3022 ssrmof 3130 rabss2 3150 rabxmdc 3364 undif4 3395 ssdif0im 3397 inssdif0im 3400 ssundifim 3416 ralf0 3436 ralm 3437 intmin4 3769 dfiin2g 3816 invdisj 3893 trint 4011 a9evsep 4020 axnul 4023 csbexga 4026 exmidn0m 4094 exmidsssn 4095 exmidsssnc 4096 exmid0el 4097 ordunisuc2r 4400 tfi 4466 peano5 4482 ssrelrel 4609 issref 4891 iotanul 5073 iota4 5076 dffun5r 5105 fv3 5412 mptfvex 5474 ssoprab2 5795 mpofvex 6069 tfri1dALT 6216 bj-nfalt 12898 elabgft1 12912 bj-rspgt 12920 bj-axemptylem 13017 bj-indind 13057 setindis 13092 bdsetindis 13094 bj-inf2vnlem1 13095 bj-inf2vn 13099 bj-inf2vn2 13100 |
Copyright terms: Public domain | W3C validator |