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 413 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imdistand 571 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: cfub 9660 cflm 9661 fzind 12069 uzss 12254 cau3lem 14704 supcvg 15201 eulerthlem2 16109 pgpfac1lem3 19130 iscnp4 21801 cncls2 21811 cncls 21812 cnntr 21813 1stcelcls 21999 cnpflf 22539 fclsnei 22557 cnpfcf 22579 alexsublem 22582 iscau4 23811 caussi 23829 equivcfil 23831 ismbf3d 24184 i1fmullem 24224 abelth 24958 ocsh 28988 fpwrelmap 30396 locfinreflem 31004 nosupbnd1lem5 33110 matunitlindf 34772 isdrngo3 35120 keridl 35193 pmapjat1 36871 |
Copyright terms: Public domain | W3C validator |