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 415 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imdistand 573 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ 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: cfub 9674 cflm 9675 fzind 12083 uzss 12268 cau3lem 14717 supcvg 15214 eulerthlem2 16122 pgpfac1lem3 19202 iscnp4 21874 cncls2 21884 cncls 21885 cnntr 21886 1stcelcls 22072 cnpflf 22612 fclsnei 22630 cnpfcf 22652 alexsublem 22655 iscau4 23885 caussi 23903 equivcfil 23905 ismbf3d 24258 i1fmullem 24298 abelth 25032 ocsh 29063 fpwrelmap 30472 locfinreflem 31108 nosupbnd1lem5 33216 matunitlindf 34894 isdrngo3 35241 keridl 35314 pmapjat1 36993 |
Copyright terms: Public domain | W3C validator |