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 140 | . 2 |
3 | 2 | ibi 175 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.21nii 678 elpr2 3519 eusv2i 4346 ffdm 5263 ov 5858 ovg 5877 nnacl 6344 elpm2r 6528 ltnqpri 7370 ltxrlt 7798 uzaddcl 9349 expcllem 10272 qexpclz 10282 1exp 10290 facnn 10441 fac0 10442 fac1 10443 bcn2 10478 znnen 11838 |
Copyright terms: Public domain | W3C validator |