![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > a2i | Unicode version |
Description: Inference derived from Axiom ax-2 7. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
a2i.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
a2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a2i.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-2 7 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-2 7 |
This theorem is referenced by: imim2i 12 mpd 13 sylcom 28 pm2.43 53 ancl 318 ancr 321 anc2r 328 pm2.65 660 pm2.18dc 856 con4biddc 858 hbim1 1581 sbcof2 1821 ralimia 2551 ceqsalg 2780 rspct 2849 elabgt 2893 fvmptt 5631 ordiso2 7068 bj-exlimmp 15007 bj-rspgt 15024 bj-indint 15169 |
Copyright terms: Public domain | W3C validator |