![]() |
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 416 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imdistand 574 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: cfub 9660 cflm 9661 fzind 12068 uzss 12253 cau3lem 14706 supcvg 15203 eulerthlem2 16109 pgpfac1lem3 19192 mhpvarcl 20798 iscnp4 21868 cncls2 21878 cncls 21879 cnntr 21880 1stcelcls 22066 cnpflf 22606 fclsnei 22624 cnpfcf 22646 alexsublem 22649 iscau4 23883 caussi 23901 equivcfil 23903 ismbf3d 24258 i1fmullem 24298 abelth 25036 ocsh 29066 fpwrelmap 30495 locfinreflem 31193 nosupbnd1lem5 33325 matunitlindf 35055 isdrngo3 35397 keridl 35470 pmapjat1 37149 |
Copyright terms: Public domain | W3C validator |