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 3693 elunii 4835 ordelord 6206 fvelrn 6836 onsucuni2 7538 fnfi 8784 prnmax 10405 relexpindlem 14410 opreu2reuALT 30167 ralssiun 34570 monotoddzz 39418 oddcomabszz 39419 flcidc 39652 syldbl2 40397 fmul01 41737 fprodcnlem 41756 stoweidlem4 42166 stoweidlem20 42182 stoweidlem22 42184 stoweidlem27 42189 stoweidlem30 42192 stoweidlem51 42213 stoweidlem59 42221 fourierdlem21 42290 fourierdlem89 42357 fourierdlem90 42358 fourierdlem91 42359 fourierdlem104 42372 |
Copyright terms: Public domain | W3C validator |