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 388 | . 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 452 anabs7 564 biadani 602 orabs 804 prlem2 963 sb6 1873 2moswapdc 2103 exsnrex 3612 eliunxp 4737 asymref 4983 elxp4 5085 elxp5 5086 dffun9 5211 funcnv 5243 funcnv3 5244 f1ompt 5630 eufnfv 5709 dff1o6 5738 abexex 6086 dfoprab4 6152 tpostpos 6223 erovlem 6584 elixp2 6659 xpsnen 6778 ctssdccl 7067 ltbtwnnq 7348 enq0enq 7363 prnmaxl 7420 prnminu 7421 elznn0nn 9196 zrevaddcl 9232 qrevaddcl 9573 climreu 11224 isprm3 12029 isprm4 12030 tgval2 12598 eltg2b 12601 isms2 13001 |
Copyright terms: Public domain | W3C validator |