| 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 390 | . 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜒 ∧ 𝜓))) | |
| 3 | 1, 2 | sylib 122 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓))) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 |
| This theorem is referenced by: ralss 3263 rexss 3264 reuhypd 4531 elxp4 5184 elxp5 5185 dfco2a 5197 feu 5475 funbrfv2b 5641 dffn5im 5642 eqfnfv2 5696 dff4im 5744 fmptco 5764 dff13 5855 f1od2 6339 mpoxopovel 6345 brtposg 6358 dftpos3 6366 erinxp 6714 qliftfun 6722 pw2f1odclem 6951 genpdflem 7650 ltexprlemm 7743 prime 9502 oddnn02np1 12276 oddge22np1 12277 evennn02n 12278 evennn2n 12279 ismgmid 13294 eqger 13645 eqgid 13647 znleval 14500 bastop2 14641 restopn2 14740 restdis 14741 tx1cn 14826 tx2cn 14827 imasnopn 14856 xmeter 14993 lgsquadlem1 15639 lgsquadlem2 15640 lgsquadlem3 15641 |
| Copyright terms: Public domain | W3C validator |