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 1440 | . 2 | |
2 | alimi.1 | . 2 | |
3 | 1, 2 | mpg 1444 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1346 |
This theorem was proved from axioms: ax-mp 5 ax-5 1440 ax-gen 1442 |
This theorem is referenced by: 2alimi 1449 al2imi 1451 alrimih 1462 hbal 1470 19.26 1474 19.33 1477 hbequid 1506 equidqe 1525 hbim 1538 hbor 1539 nford 1560 nfand 1561 nfal 1569 nfalt 1571 19.21ht 1574 exbi 1597 19.29 1613 19.25 1619 alexim 1638 alexnim 1641 19.9hd 1655 19.32r 1673 ax10 1710 spimh 1730 equvini 1751 nfexd 1754 stdpc4 1768 ax10oe 1790 sbcof2 1803 sb4bor 1828 nfsb2or 1830 spsbim 1836 ax16i 1851 sbi2v 1885 nfsbt 1969 nfsbd 1970 sbalyz 1992 hbsb4t 2006 dvelimor 2011 sbal2 2013 mo2n 2047 eumo0 2050 mor 2061 bm1.1 2155 alral 2515 rgen2a 2524 ralimi2 2530 rexim 2564 r19.32r 2616 ceqsalt 2756 spcgft 2807 spcegft 2809 spc2gv 2821 spc3gv 2823 rspct 2827 elabgt 2871 reu6 2919 sbciegft 2985 csbeq2 3073 csbnestgf 3101 ssrmof 3210 rabss2 3230 rabxmdc 3446 undif4 3477 ssdif0im 3479 inssdif0im 3482 ssundifim 3498 ralf0 3518 ralm 3519 intmin4 3859 dfiin2g 3906 invdisj 3983 trint 4102 a9evsep 4111 axnul 4114 csbexga 4117 exmidn0m 4187 exmidsssn 4188 exmidsssnc 4189 exmid0el 4190 ordunisuc2r 4498 tfi 4566 peano5 4582 ssrelrel 4711 issref 4993 iotanul 5175 iota4 5178 dffun5r 5210 fv3 5519 mptfvex 5581 ssoprab2 5909 mpofvex 6182 tfri1dALT 6330 prodeq2w 11519 bj-nfalt 13799 elabgft1 13813 bj-rspgt 13821 bj-axemptylem 13927 bj-indind 13967 setindis 14002 bdsetindis 14004 bj-inf2vnlem1 14005 bj-inf2vn 14009 bj-inf2vn2 14010 |
Copyright terms: Public domain | W3C validator |