Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm5.32d | GIF version |
Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
pm5.32d.1 | ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
Ref | Expression |
---|---|
pm5.32d | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32d.1 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | |
2 | biimp 117 | . . . 4 ⊢ ((𝜒 ↔ 𝜃) → (𝜒 → 𝜃)) | |
3 | 1, 2 | syl6 33 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
4 | 3 | imdistand 444 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃))) |
5 | biimpr 129 | . . . 4 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 → 𝜒)) | |
6 | 1, 5 | syl6 33 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
7 | 6 | imdistand 444 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜓 ∧ 𝜒))) |
8 | 4, 7 | impbid 128 | 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: pm5.32rd 447 pm5.32da 448 pm5.32 449 anbi2d 460 cbvex2 1909 cores 5104 isoini 5783 mpoeq123 5895 genpassl 7459 genpassu 7460 fzind 9300 btwnz 9304 elfzm11 10020 isprm2 12043 isprm3 12044 modprminv 12175 modprminveq 12176 |
Copyright terms: Public domain | W3C validator |