Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm4.71ri | Unicode version |
Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.) |
Ref | Expression |
---|---|
pm4.71ri.1 |
Ref | Expression |
---|---|
pm4.71ri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.71ri.1 | . 2 | |
2 | pm4.71r 387 | . 2 | |
3 | 1, 2 | mpbi 144 | 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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biadan2 451 anabs7 548 biadani 586 orabs 788 prlem2 943 sb6 1842 2moswapdc 2067 exsnrex 3536 eliunxp 4648 asymref 4894 elxp4 4996 elxp5 4997 dffun9 5122 funcnv 5154 funcnv3 5155 f1ompt 5539 eufnfv 5616 dff1o6 5645 abexex 5992 dfoprab4 6058 tpostpos 6129 erovlem 6489 elixp2 6564 xpsnen 6683 ctssdccl 6964 ltbtwnnq 7192 enq0enq 7207 prnmaxl 7264 prnminu 7265 elznn0nn 9036 zrevaddcl 9072 qrevaddcl 9404 climreu 11034 isprm3 11726 isprm4 11727 tgval2 12147 eltg2b 12150 isms2 12550 |
Copyright terms: Public domain | W3C validator |