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 561 pm4.45 773 unidif0 4091 sucexb 4413 imadmrn 4891 dff1o2 5372 xpsnen 6715 dmaddpq 7187 dmmulpq 7188 eqreznegel 9406 xrnemnf 9564 xrnepnf 9565 elioopnf 9750 elioomnf 9751 elicopnf 9752 elxrge0 9761 isprm2 11798 bj-sucexg 13120 |
Copyright terms: Public domain | W3C validator |