![]() |
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 449 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imdistand 728 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ 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: cfub 9109 cflm 9110 fzind 11513 uzss 11746 cau3lem 14138 supcvg 14632 eulerthlem2 15534 pgpfac1lem3 18522 iscnp4 21115 cncls2 21125 cncls 21126 cnntr 21127 1stcelcls 21312 cnpflf 21852 fclsnei 21870 cnpfcf 21892 alexsublem 21895 iscau4 23123 caussi 23141 equivcfil 23143 ismbf3d 23466 i1fmullem 23506 abelth 24240 ocsh 28270 fpwrelmap 29636 locfinreflem 30035 nosupbnd1lem5 31983 matunitlindf 33537 isdrngo3 33888 keridl 33961 pmapjat1 35457 |
Copyright terms: Public domain | W3C validator |