![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm5.32d | Structured version Visualization version GIF version |
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 29-Oct-1996.) |
Ref | Expression |
---|---|
pm5.32d.1 | ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
Ref | Expression |
---|---|
pm5.32d | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32d.1 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | |
2 | pm5.32 671 | . 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) | |
3 | 1, 2 | sylib 208 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 |
This theorem is referenced by: pm5.32rd 675 pm5.32da 676 anbi2d 742 raltpd 4458 dfres3 5556 cores 5799 isoini 6751 mpt2eq123 6879 ordpwsuc 7180 rdglim2 7697 fzind 11667 btwnz 11671 elfzm11 12604 isprm2 15597 isprm3 15598 modprminv 15706 modprminveq 15707 isrim 18935 elimifd 29669 funcnvmptOLD 29776 xrecex 29937 ordtconnlem1 30279 indpi1 30391 dfrdg4 32364 ee7.2aOLD 32766 wl-ax11-lem8 33682 expdioph 38092 pm14.122b 39126 rexbidar 39152 mapsnend 39890 isrngim 42414 |
Copyright terms: Public domain | W3C validator |