![]() |
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 3664 elunii 4871 ordelord 6340 fvelrn 7028 onsucuni2 7770 fnfi 9128 prnmax 10936 relexpindlem 14954 opreu2reuALT 31448 ralssiun 35924 monotoddzz 41310 oddcomabszz 41311 flcidc 41544 fmul01 43907 fprodcnlem 43926 stoweidlem4 44331 stoweidlem20 44347 stoweidlem22 44349 stoweidlem27 44354 stoweidlem30 44357 stoweidlem51 44378 stoweidlem59 44386 fourierdlem21 44455 fourierdlem89 44522 fourierdlem90 44523 fourierdlem91 44524 fourierdlem104 44537 |
Copyright terms: Public domain | W3C validator |