|   | 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 670 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒) | 
| 3 | 2 | ancoms 458 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: syldbl2 841 nelrdva 3710 elunii 4911 ordelord 6405 fvelrn 7095 onsucuni2 7855 fnfi 9219 prnmax 11036 relexpindlem 15103 opreu2reuALT 32497 ralssiun 37409 monotoddzz 42960 oddcomabszz 42961 flcidc 43187 fmul01 45600 fprodcnlem 45619 stoweidlem4 46024 stoweidlem20 46040 stoweidlem22 46042 stoweidlem27 46047 stoweidlem30 46050 stoweidlem51 46071 stoweidlem59 46079 fourierdlem21 46148 fourierdlem89 46215 fourierdlem90 46216 fourierdlem91 46217 fourierdlem104 46230 | 
| Copyright terms: Public domain | W3C validator |