![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm4.71rd | GIF version |
Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.) |
Ref | Expression |
---|---|
pm4.71rd.1 | ⊢ (φ → (ψ → χ)) |
Ref | Expression |
---|---|
pm4.71rd | ⊢ (φ → (ψ ↔ (χ ∧ ψ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.71rd.1 | . 2 ⊢ (φ → (ψ → χ)) | |
2 | pm4.71r 370 | . 2 ⊢ ((ψ → χ) ↔ (ψ ↔ (χ ∧ ψ))) | |
3 | 1, 2 | sylib 127 | 1 ⊢ (φ → (ψ ↔ (χ ∧ ψ))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ralss 3000 rexss 3001 reuhypd 4169 elxp4 4751 elxp5 4752 dfco2a 4764 feu 5015 funbrfv2b 5161 dffn5im 5162 eqfnfv2 5209 dff4im 5256 fmptco 5273 dff13 5350 mpt2xopovel 5797 brtposg 5810 dftpos3 5818 erinxp 6116 qliftfun 6124 genpdflem 6490 ltexprlemm 6574 prime 8113 |
Copyright terms: Public domain | W3C validator |