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 form). (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 576 | . 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) | |
3 | 1, 2 | sylib 220 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: pm5.32rd 580 pm5.32da 581 anbi2d 630 ralrexbid 3322 raltpd 4709 opeqsng 5385 dfres3 5852 cores 6096 isoini 7085 mpoeq123 7220 ordpwsuc 7524 rdglim2 8062 fzind 12074 btwnz 12078 elfzm11 12972 isprm2 16020 isprm3 16021 modprminv 16130 modprminveq 16131 isrim 19479 elimifd 30292 xrecex 30591 ordtconnlem1 31162 indpi1 31274 eqfunresadj 32999 dfrdg4 33407 ee7.2aOLD 33804 wl-ax11-lem8 34818 expdioph 39613 pm14.122b 40748 rexbidar 40771 isrngim 44169 |
Copyright terms: Public domain | W3C validator |