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 381 | . 2 | |
3 | 1, 2 | mpbi 143 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: pm4.24 387 anabs1 536 pm4.45 730 unidif0 3941 sucexb 4241 imadmrn 4698 dff1o2 5151 xpsnen 6318 dmaddpq 6569 dmmulpq 6570 eqreznegel 8699 xrnemnf 8853 xrnepnf 8854 elioopnf 8990 elioomnf 8991 elicopnf 8992 elxrge0 9001 isprm2 10499 bj-sucexg 10713 |
Copyright terms: Public domain | W3C validator |