![]() |
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 390 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 145 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: biadan2 456 anabs7 574 biadani 612 orabs 814 prlem2 974 sb6 1886 2moswapdc 2116 exsnrex 3633 eliunxp 4761 asymref 5009 elxp4 5111 elxp5 5112 dffun9 5240 funcnv 5272 funcnv3 5273 f1ompt 5662 eufnfv 5741 dff1o6 5770 abexex 6120 dfoprab4 6186 tpostpos 6258 erovlem 6620 elixp2 6695 xpsnen 6814 ctssdccl 7103 ltbtwnnq 7393 enq0enq 7408 prnmaxl 7465 prnminu 7466 elznn0nn 9243 zrevaddcl 9279 qrevaddcl 9620 climreu 11276 isprm3 12088 isprm4 12089 tgval2 13184 eltg2b 13187 isms2 13587 |
Copyright terms: Public domain | W3C validator |