Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm4.71i | GIF 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 546 pm4.45 758 unidif0 4061 sucexb 4383 imadmrn 4861 dff1o2 5340 xpsnen 6683 dmaddpq 7155 dmmulpq 7156 eqreznegel 9374 xrnemnf 9532 xrnepnf 9533 elioopnf 9718 elioomnf 9719 elicopnf 9720 elxrge0 9729 isprm2 11725 bj-sucexg 13047 |
Copyright terms: Public domain | W3C validator |