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 126 | . 2 | |
2 | simpr 103 | . 2 | |
3 | 1, 2 | impbid1 130 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: biantrur 287 biantrurd 289 anclb 302 pm5.42 303 pm5.32 426 anabs5 507 pm5.33 541 bianabs 543 baib 828 baibd 832 anxordi 1291 euan 1956 eueq3dc 2715 xpcom 4864 fvopab3g 5245 riota1a 5487 recmulnqg 6489 ltexprlemloc 6705 eluz2 8479 rpnegap 8615 elfz2 8881 shftfib 9424 |
Copyright terms: Public domain | W3C validator |