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 1427 | . 2 | |
2 | alimi.1 | . 2 | |
3 | 1, 2 | mpg 1431 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1333 |
This theorem was proved from axioms: ax-mp 5 ax-5 1427 ax-gen 1429 |
This theorem is referenced by: 2alimi 1436 al2imi 1438 alrimih 1449 hbal 1457 19.26 1461 19.33 1464 hbequid 1493 equidqe 1512 hbim 1525 hbor 1526 nford 1547 nfand 1548 nfal 1556 nfalt 1558 19.21ht 1561 exbi 1584 19.29 1600 19.25 1606 alexim 1625 alexnim 1628 19.9hd 1642 19.32r 1660 ax10 1697 spimh 1717 equvini 1738 nfexd 1741 stdpc4 1755 ax10oe 1777 sbcof2 1790 sb4bor 1815 nfsb2or 1817 spsbim 1823 ax16i 1838 sbi2v 1872 nfsbt 1956 nfsbd 1957 sbalyz 1979 hbsb4t 1993 dvelimor 1998 sbal2 2000 mo2n 2034 eumo0 2037 mor 2048 bm1.1 2142 alral 2502 rgen2a 2511 ralimi2 2517 rexim 2551 r19.32r 2603 ceqsalt 2738 spcgft 2789 spcegft 2791 spc2gv 2803 spc3gv 2805 rspct 2809 elabgt 2853 reu6 2901 sbciegft 2967 csbeq2 3055 csbnestgf 3083 ssrmof 3191 rabss2 3211 rabxmdc 3425 undif4 3456 ssdif0im 3458 inssdif0im 3461 ssundifim 3477 ralf0 3497 ralm 3498 intmin4 3835 dfiin2g 3882 invdisj 3959 trint 4077 a9evsep 4086 axnul 4089 csbexga 4092 exmidn0m 4162 exmidsssn 4163 exmidsssnc 4164 exmid0el 4165 ordunisuc2r 4473 tfi 4541 peano5 4557 ssrelrel 4686 issref 4968 iotanul 5150 iota4 5153 dffun5r 5182 fv3 5491 mptfvex 5553 ssoprab2 5877 mpofvex 6151 tfri1dALT 6298 prodeq2w 11453 bj-nfalt 13349 elabgft1 13363 bj-rspgt 13371 bj-axemptylem 13478 bj-indind 13518 setindis 13553 bdsetindis 13555 bj-inf2vnlem1 13556 bj-inf2vn 13560 bj-inf2vn2 13561 |
Copyright terms: Public domain | W3C validator |