| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > imdistanda | Structured version Visualization version GIF version | ||
| Description: Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.) |
| Ref | Expression |
|---|---|
| imdistanda.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
| Ref | Expression |
|---|---|
| imdistanda | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imdistanda.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | |
| 2 | 1 | ex 412 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
| 3 | 2 | imdistand 570 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: predtrss 6343 cfub 10289 cflm 10290 fzind 12716 uzss 12901 cau3lem 15393 supcvg 15892 eulerthlem2 16819 pgpfac1lem3 20097 iscnp4 23271 cncls2 23281 cncls 23282 cnntr 23283 1stcelcls 23469 cnpflf 24009 fclsnei 24027 cnpfcf 24049 alexsublem 24052 iscau4 25313 caussi 25331 equivcfil 25333 ismbf3d 25689 i1fmullem 25729 abelth 26485 nosupbnd1lem5 27757 ocsh 31302 fpwrelmap 32744 locfinreflem 33839 matunitlindf 37625 isdrngo3 37966 keridl 38039 pmapjat1 39855 |
| Copyright terms: Public domain | W3C validator |