![]() |
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 669 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
3 | 2 | ancoms 460 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: syldbl2 840 nelrdva 3702 elunii 4914 ordelord 6387 fvelrn 7079 onsucuni2 7822 fnfi 9181 prnmax 10990 relexpindlem 15010 opreu2reuALT 31748 ralssiun 36336 monotoddzz 41730 oddcomabszz 41731 flcidc 41964 fmul01 44344 fprodcnlem 44363 stoweidlem4 44768 stoweidlem20 44784 stoweidlem22 44786 stoweidlem27 44791 stoweidlem30 44794 stoweidlem51 44815 stoweidlem59 44823 fourierdlem21 44892 fourierdlem89 44959 fourierdlem90 44960 fourierdlem91 44961 fourierdlem104 44974 |
Copyright terms: Public domain | W3C validator |