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 666 | . 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 208 df-an 397 |
This theorem is referenced by: nelrdva 3695 elunii 4837 ordelord 6207 fvelrn 6837 onsucuni2 7537 fnfi 8785 prnmax 10406 relexpindlem 14412 opreu2reuALT 30168 ralssiun 34571 monotoddzz 39420 oddcomabszz 39421 flcidc 39654 syldbl2 40399 fmul01 41741 fprodcnlem 41760 stoweidlem4 42170 stoweidlem20 42186 stoweidlem22 42188 stoweidlem27 42193 stoweidlem30 42196 stoweidlem51 42217 stoweidlem59 42225 fourierdlem21 42294 fourierdlem89 42361 fourierdlem90 42362 fourierdlem91 42363 fourierdlem104 42376 |
Copyright terms: Public domain | W3C validator |