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: predtrss 6197 cfub 9887 cflm 9888 fzind 12299 uzss 12485 cau3lem 14942 supcvg 15444 eulerthlem2 16359 pgpfac1lem3 19488 iscnp4 22184 cncls2 22194 cncls 22195 cnntr 22196 1stcelcls 22382 cnpflf 22922 fclsnei 22940 cnpfcf 22962 alexsublem 22965 iscau4 24200 caussi 24218 equivcfil 24220 ismbf3d 24575 i1fmullem 24615 abelth 25357 ocsh 29388 fpwrelmap 30812 locfinreflem 31528 nosupbnd1lem5 33678 matunitlindf 35538 isdrngo3 35880 keridl 35953 pmapjat1 37630 |
Copyright terms: Public domain | W3C validator |