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: wi 4 |
This theorem was proved from axioms: ax-2 6 ax-mp 7 |
This theorem is referenced by: imim2i 12 mpd 13 sylcom 25 pm2.43 47 ancl 301 ancr 304 anc2r 311 pm2.65 585 pm2.18dc 750 con4biddc 754 hbim1 1462 sbcof2 1691 ralimia 2382 ceqsalg 2582 rspct 2649 elabgt 2684 fvmptt 5262 ordiso2 6357 bj-exlimmp 9909 bj-rspgt 9925 bj-indint 10055 |
Copyright terms: Public domain | W3C validator |