![]() |
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 388 | . 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜒 ∧ 𝜓))) | |
3 | 1, 2 | sylib 121 | 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: ralss 3168 rexss 3169 reuhypd 4400 elxp4 5034 elxp5 5035 dfco2a 5047 feu 5313 funbrfv2b 5474 dffn5im 5475 eqfnfv2 5527 dff4im 5574 fmptco 5594 dff13 5677 f1od2 6140 mpoxopovel 6146 brtposg 6159 dftpos3 6167 erinxp 6511 qliftfun 6519 genpdflem 7339 ltexprlemm 7432 prime 9174 oddnn02np1 11613 oddge22np1 11614 evennn02n 11615 evennn2n 11616 bastop2 12292 restopn2 12391 restdis 12392 tx1cn 12477 tx2cn 12478 imasnopn 12507 xmeter 12644 |
Copyright terms: Public domain | W3C validator |