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 369 | . 2 | |
3 | 1, 2 | mpbi 133 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wb 98 |
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: pm4.24 375 anabs1 506 pm4.45 698 unidif0 3920 sucexb 4223 imadmrn 4678 dff1o2 5131 xpsnen 6295 dmaddpq 6477 dmmulpq 6478 eqreznegel 8549 xrnemnf 8699 xrnepnf 8700 elioopnf 8836 elioomnf 8837 elicopnf 8838 elxrge0 8847 bj-sucexg 10042 |
Copyright terms: Public domain | W3C validator |