![]() |
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 2315 reubida 2485 rmobida 2490 mpteq12f 3828 reuhypd 4169 funbrfv2b 5161 dffn5im 5162 eqfnfv2 5209 fndmin 5217 fniniseg 5230 rexsupp 5234 fmptco 5273 dff13 5350 riotabidva 5427 mpt2eq123dva 5508 mpt2eq3dva 5511 mpt2xopovel 5797 qliftfun 6124 erovlem 6134 xpcomco 6236 ltexpi 6321 dfplpq2 6338 axprecex 6764 zrevaddcl 8071 qrevaddcl 8353 icoshft 8628 fznn 8721 |
Copyright terms: Public domain | W3C validator |