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 388 | . 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: biadan2 453 anabs7 569 biadani 607 orabs 809 prlem2 969 sb6 1879 2moswapdc 2109 exsnrex 3625 eliunxp 4750 asymref 4996 elxp4 5098 elxp5 5099 dffun9 5227 funcnv 5259 funcnv3 5260 f1ompt 5647 eufnfv 5726 dff1o6 5755 abexex 6105 dfoprab4 6171 tpostpos 6243 erovlem 6605 elixp2 6680 xpsnen 6799 ctssdccl 7088 ltbtwnnq 7378 enq0enq 7393 prnmaxl 7450 prnminu 7451 elznn0nn 9226 zrevaddcl 9262 qrevaddcl 9603 climreu 11260 isprm3 12072 isprm4 12073 tgval2 12845 eltg2b 12848 isms2 13248 |
Copyright terms: Public domain | W3C validator |