![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anabsi7 | Structured version Visualization version GIF version |
Description: Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.) |
Ref | Expression |
---|---|
anabsi7.1 | ⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒)) |
Ref | Expression |
---|---|
anabsi7 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anabsi7.1 | . . 3 ⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒)) | |
2 | 1 | anabsi6 668 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
3 | 2 | ancoms 459 | 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 206 df-an 397 |
This theorem is referenced by: syldbl2 839 nelrdva 3697 elunii 4906 ordelord 6375 fvelrn 7063 onsucuni2 7805 fnfi 9164 prnmax 10972 relexpindlem 14992 opreu2reuALT 31580 ralssiun 36092 monotoddzz 41453 oddcomabszz 41454 flcidc 41687 fmul01 44069 fprodcnlem 44088 stoweidlem4 44493 stoweidlem20 44509 stoweidlem22 44511 stoweidlem27 44516 stoweidlem30 44519 stoweidlem51 44540 stoweidlem59 44548 fourierdlem21 44617 fourierdlem89 44684 fourierdlem90 44685 fourierdlem91 44686 fourierdlem104 44699 |
Copyright terms: Public domain | W3C validator |