![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm4.71ri | GIF version |
Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.) |
Ref | Expression |
---|---|
pm4.71ri.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
pm4.71ri | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.71ri.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | pm4.71r 383 | . 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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biadan2 445 anabs7 542 biadani 580 orabs 766 prlem2 923 sb6 1821 2moswapdc 2045 exsnrex 3505 eliunxp 4606 asymref 4850 elxp4 4952 elxp5 4953 dffun9 5078 funcnv 5109 funcnv3 5110 f1ompt 5489 eufnfv 5564 dff1o6 5593 abexex 5935 dfoprab4 6000 tpostpos 6067 erovlem 6424 elixp2 6499 xpsnen 6617 ltbtwnnq 7072 enq0enq 7087 prnmaxl 7144 prnminu 7145 elznn0nn 8862 zrevaddcl 8898 qrevaddcl 9228 climreu 10840 isprm3 11527 isprm4 11528 tgval2 11903 eltg2b 11906 isms2 12240 |
Copyright terms: Public domain | W3C validator |