![]() |
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 3221 rexss 3222 reuhypd 4468 elxp4 5112 elxp5 5113 dfco2a 5125 feu 5394 funbrfv2b 5556 dffn5im 5557 eqfnfv2 5610 dff4im 5658 fmptco 5678 dff13 5763 f1od2 6230 mpoxopovel 6236 brtposg 6249 dftpos3 6257 erinxp 6603 qliftfun 6611 genpdflem 7494 ltexprlemm 7587 prime 9338 oddnn02np1 11865 oddge22np1 11866 evennn02n 11867 evennn2n 11868 ismgmid 12685 bastop2 13248 restopn2 13347 restdis 13348 tx1cn 13433 tx2cn 13434 imasnopn 13463 xmeter 13600 |
Copyright terms: Public domain | W3C validator |