![]() |
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 385 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 144 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biadan2 449 anabs7 546 biadani 584 orabs 786 prlem2 941 sb6 1840 2moswapdc 2065 exsnrex 3532 eliunxp 4638 asymref 4882 elxp4 4984 elxp5 4985 dffun9 5110 funcnv 5142 funcnv3 5143 f1ompt 5525 eufnfv 5602 dff1o6 5631 abexex 5978 dfoprab4 6044 tpostpos 6115 erovlem 6475 elixp2 6550 xpsnen 6668 ctssdccl 6948 ltbtwnnq 7172 enq0enq 7187 prnmaxl 7244 prnminu 7245 elznn0nn 8972 zrevaddcl 9008 qrevaddcl 9338 climreu 10958 isprm3 11645 isprm4 11646 tgval2 12063 eltg2b 12066 isms2 12443 |
Copyright terms: Public domain | W3C validator |