| 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 1470 |
. 2
| |
| 2 | alimi.1 |
. 2
| |
| 3 | 1, 2 | mpg 1474 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-5 1470 ax-gen 1472 |
| This theorem is referenced by: 2alimi 1479 al2imi 1481 alrimih 1492 hbal 1500 19.26 1504 19.33 1507 hbequid 1536 equidqe 1555 hbim 1568 hbor 1569 nford 1590 nfand 1591 nfal 1599 nfalt 1601 19.21ht 1604 exbi 1627 19.29 1643 19.25 1649 alexim 1668 alexnim 1671 19.9hd 1685 19.32r 1703 ax10 1740 spimh 1760 equvini 1781 nfexd 1784 stdpc4 1798 ax10oe 1820 sbcof2 1833 sb4bor 1858 nfsb2or 1860 spsbim 1866 ax16i 1881 sbi2v 1916 nfsbt 2004 nfsbd 2005 sbalyz 2027 hbsb4t 2041 dvelimor 2046 sbal2 2048 mo2n 2082 eumo0 2085 mor 2096 bm1.1 2190 alral 2551 rgen2a 2560 ralimi2 2566 rexim 2600 r19.32r 2652 ceqsalt 2798 spcgft 2850 spcegft 2852 spc2gv 2864 spc3gv 2866 rspct 2870 elabgt 2914 reu6 2962 sbciegft 3029 csbeq2 3117 csbnestgf 3146 ssrmof 3256 rabss2 3276 rabxmdc 3492 undif4 3523 ssdif0im 3525 inssdif0im 3528 ssundifim 3544 ralf0 3563 ralm 3564 intmin4 3913 dfiin2g 3960 invdisj 4038 trint 4157 a9evsep 4166 axnul 4169 csbexga 4172 exmidn0m 4245 exmidsssn 4246 exmidsssnc 4247 exmid0el 4248 ordunisuc2r 4562 tfi 4630 peano5 4646 ssrelrel 4775 issref 5065 iotanul 5247 iota4 5251 dffun5r 5283 fundif 5318 fv3 5599 mptfvex 5665 ssoprab2 6001 mpofvex 6291 tfri1dALT 6437 prodeq2w 11867 bj-nfalt 15700 elabgft1 15714 bj-rspgt 15722 bj-axemptylem 15828 bj-indind 15868 setindis 15903 bdsetindis 15905 bj-inf2vnlem1 15906 bj-inf2vn 15910 bj-inf2vn2 15911 |
| Copyright terms: Public domain | W3C validator |