![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ibir | Unicode version |
Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.) |
Ref | Expression |
---|---|
ibir.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ibir |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ibir.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bicomd 141 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ibi 176 |
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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm5.21nii 704 elpr2 3613 eusv2i 4452 ffdm 5382 ov 5988 ovg 6007 nnacl 6475 elpm2r 6660 ltnqpri 7581 ltxrlt 8010 uzaddcl 9572 expcllem 10514 qexpclz 10524 1exp 10532 facnn 10688 fac0 10689 fac1 10690 bcn2 10725 znnen 12379 |
Copyright terms: Public domain | W3C validator |