New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 612 | . 2 ⊢ ((φ → ψ) ↔ (φ ↔ (ψ ∧ φ))) | |
3 | 1, 2 | mpbi 199 | 1 ⊢ (φ ↔ (ψ ∧ φ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 ∧ wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: biadan2 623 anabs7 785 orabs 828 prlem2 929 sb6 2099 2moswap 2279 opkelimagekg 4271 dfpw12 4301 dfnnc2 4395 eliunxp 4821 elres 4995 imadmrn 5008 elxp4 5108 dffun9 5135 funcnv 5156 funcnv3 5157 dff1o6 5475 txpcofun 5803 |
Copyright terms: Public domain | W3C validator |