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 138 | . 2 | |
2 | simpr 109 | . 2 | |
3 | 1, 2 | impbid1 141 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biantrur 301 biantrurd 303 anclb 317 pm5.42 318 pm5.32 448 anabs5 547 pm5.33 583 bianabs 585 baib 889 baibd 893 anxordi 1363 euan 2033 eueq3dc 2831 ifandc 3478 xpcom 5055 fvopab3g 5462 riota1a 5717 ctssdccl 6964 recmulnqg 7167 ltexprlemloc 7383 mul0eqap 8399 eluz2 9300 rpnegap 9442 elfz2 9765 zmodid2 10093 shftfib 10563 dvdsssfz1 11477 modremain 11553 ctiunctlemudc 11877 txcnmpt 12369 reopnap 12634 ellimc3apf 12725 |
Copyright terms: Public domain | W3C validator |