![]() |
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 387 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 144 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm4.24 393 anabs1 562 pm4.45 774 unidif0 4099 sucexb 4421 imadmrn 4899 dff1o2 5380 xpsnen 6723 dmaddpq 7211 dmmulpq 7212 eqreznegel 9433 xrnemnf 9594 xrnepnf 9595 elioopnf 9780 elioomnf 9781 elicopnf 9782 elxrge0 9791 isprm2 11834 bj-sucexg 13291 |
Copyright terms: Public domain | W3C validator |