![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > a2i | Unicode version |
Description: Inference derived from axiom ax-2 6. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
a2i.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
a2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a2i.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-2 6 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-2 6 ax-mp 7 |
This theorem is referenced by: imim2i 12 mpd 13 sylcom 28 pm2.43 53 ancl 312 ancr 315 anc2r 322 pm2.65 621 pm2.18dc 789 con4biddc 793 hbim1 1508 sbcof2 1739 ralimia 2437 ceqsalg 2648 rspct 2716 elabgt 2758 fvmptt 5407 ordiso2 6782 bj-exlimmp 11936 bj-rspgt 11952 bj-indint 12092 |
Copyright terms: Public domain | W3C validator |