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 855 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
3 | 2 | ancoms 468 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: syl2an23an 1379 nelrdva 3384 elunii 4377 ordelord 5662 fvelrn 6260 onsucuni2 6926 fnfi 8123 prnmax 9696 monotoddzz 36526 oddcomabszz 36527 flcidc 36763 syldbl2 37490 fmul01 38647 fprodcnlem 38666 stoweidlem4 38897 stoweidlem20 38913 stoweidlem22 38915 stoweidlem27 38920 stoweidlem30 38923 stoweidlem51 38944 stoweidlem59 38952 fourierdlem21 39021 fourierdlem89 39088 fourierdlem90 39089 fourierdlem91 39090 fourierdlem104 39103 |
Copyright terms: Public domain | W3C validator |