Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm4.71i | Unicode version |
Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.) |
Ref | Expression |
---|---|
pm4.71i.1 |
Ref | Expression |
---|---|
pm4.71i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.71i.1 | . 2 | |
2 | pm4.71 386 | . 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: pm4.24 392 anabs1 561 pm4.45 773 unidif0 4086 sucexb 4408 imadmrn 4886 dff1o2 5365 xpsnen 6708 dmaddpq 7180 dmmulpq 7181 eqreznegel 9399 xrnemnf 9557 xrnepnf 9558 elioopnf 9743 elioomnf 9744 elicopnf 9745 elxrge0 9754 isprm2 11787 bj-sucexg 13109 |
Copyright terms: Public domain | W3C validator |