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 3623 eliunxp 4748 asymref 4994 elxp4 5096 elxp5 5097 dffun9 5225 funcnv 5257 funcnv3 5258 f1ompt 5645 eufnfv 5724 dff1o6 5753 abexex 6103 dfoprab4 6169 tpostpos 6241 erovlem 6603 elixp2 6678 xpsnen 6797 ctssdccl 7086 ltbtwnnq 7371 enq0enq 7386 prnmaxl 7443 prnminu 7444 elznn0nn 9219 zrevaddcl 9255 qrevaddcl 9596 climreu 11253 isprm3 12065 isprm4 12066 tgval2 12810 eltg2b 12813 isms2 13213 |
Copyright terms: Public domain | W3C validator |