![]() |
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 139 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | simpr 110 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbid1 142 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: biantrur 303 biantrurd 305 anclb 319 pm5.42 320 pm5.32 453 anabs5 573 pm5.33 609 bianabs 611 baib 920 baibd 924 anxordi 1411 euan 2094 eueq3dc 2926 ifandc 3587 xpcom 5193 fvopab3g 5610 riota1a 5871 ctssdccl 7140 2omotaplemap 7286 recmulnqg 7420 ltexprlemloc 7636 mul0eqap 8657 eluz2 9564 rpnegap 9716 elfz2 10045 zmodid2 10383 shftfib 10864 dvdsssfz1 11890 modremain 11966 phisum 12272 ctiunctlemudc 12488 issubg 13112 resgrpisgrp 13134 qusecsub 13268 issubrng 13546 issubrg 13568 txcnmpt 14230 reopnap 14495 ellimc3apf 14586 |
Copyright terms: Public domain | W3C validator |