![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ibar | Unicode version |
Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) (Revised by NM, 24-Mar-2013.) |
Ref | Expression |
---|---|
ibar |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2 137 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | simpr 108 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbid1 140 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: biantrur 297 biantrurd 299 anclb 312 pm5.42 313 pm5.32 441 anabs5 540 pm5.33 576 bianabs 578 baib 866 baibd 870 anxordi 1336 euan 2004 eueq3dc 2789 ifandc 3427 xpcom 4977 fvopab3g 5377 riota1a 5627 recmulnqg 6948 ltexprlemloc 7164 eluz2 9023 rpnegap 9164 elfz2 9429 zmodid2 9755 shftfib 10253 dvdsssfz1 11127 modremain 11203 |
Copyright terms: Public domain | W3C validator |