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 108 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
3 | 2 | pm5.32d 423 | 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: rexbida 2321 reubida 2491 rmobida 2496 mpteq12f 3837 reuhypd 4203 funbrfv2b 5218 dffn5im 5219 eqfnfv2 5266 fndmin 5274 fniniseg 5287 rexsupp 5291 fmptco 5330 dff13 5407 riotabidva 5484 mpt2eq123dva 5566 mpt2eq3dva 5569 mpt2xopovel 5856 qliftfun 6188 erovlem 6198 xpcomco 6300 ltexpi 6435 dfplpq2 6452 axprecex 6954 zrevaddcl 8295 qrevaddcl 8578 icoshft 8858 fznn 8951 shftdm 9423 2shfti 9432 |
Copyright terms: Public domain | W3C validator |