![]() |
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 370 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 133 |
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 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: biadan2 429 anabs7 508 orabs 726 prlem2 880 sb6 1763 2moswapdc 1987 exsnrex 3404 eliunxp 4418 asymref 4653 elxp4 4751 elxp5 4752 dffun9 4873 funcnv 4903 funcnv3 4904 f1ompt 5263 eufnfv 5332 dff1o6 5359 abexex 5695 dfoprab4 5760 tpostpos 5820 erovlem 6134 xpsnen 6231 ltbtwnnq 6399 enq0enq 6414 prnmaxl 6471 prnminu 6472 elznn0nn 8035 zrevaddcl 8071 qrevaddcl 8353 |
Copyright terms: Public domain | W3C validator |