![]() |
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 815 prlem2 975 sb6 1896 2moswapdc 2126 exsnrex 3646 eliunxp 4778 asymref 5026 elxp4 5128 elxp5 5129 dffun9 5257 funcnv 5289 funcnv3 5290 f1ompt 5680 eufnfv 5760 dff1o6 5790 abexex 6140 dfoprab4 6206 tpostpos 6278 erovlem 6640 elixp2 6715 xpsnen 6834 ctssdccl 7123 ltbtwnnq 7428 enq0enq 7443 prnmaxl 7500 prnminu 7501 elznn0nn 9280 zrevaddcl 9316 qrevaddcl 9657 climreu 11318 isprm3 12131 isprm4 12132 xpscf 12784 tgval2 13791 eltg2b 13794 isms2 14194 |
Copyright terms: Public domain | W3C validator |