![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm5.32da | GIF version |
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.) |
Ref | Expression |
---|---|
pm5.32da.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
pm5.32da | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32da.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | ex 113 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
3 | 2 | pm5.32d 438 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: rexbida 2368 reubida 2540 rmobida 2545 mpteq12f 3878 reuhypd 4249 funbrfv2b 5271 dffn5im 5272 eqfnfv2 5319 fndmin 5327 fniniseg 5340 rexsupp 5344 fmptco 5383 dff13 5460 riotabidva 5536 mpt2eq123dva 5618 mpt2eq3dva 5621 mpt2xopovel 5911 qliftfun 6276 erovlem 6286 xpcomco 6392 ltexpi 6659 dfplpq2 6676 axprecex 7178 zrevaddcl 8552 qrevaddcl 8880 icoshft 9158 fznn 9252 shftdm 9929 2shfti 9938 sumeq2d 10415 sumeq2 10416 gcdaddm 10600 |
Copyright terms: Public domain | W3C validator |