![]() |
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 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 840 nelrdva 3727 elunii 4936 ordelord 6417 fvelrn 7110 onsucuni2 7870 fnfi 9244 prnmax 11064 relexpindlem 15112 opreu2reuALT 32505 ralssiun 37373 monotoddzz 42900 oddcomabszz 42901 flcidc 43131 fmul01 45501 fprodcnlem 45520 stoweidlem4 45925 stoweidlem20 45941 stoweidlem22 45943 stoweidlem27 45948 stoweidlem30 45951 stoweidlem51 45972 stoweidlem59 45980 fourierdlem21 46049 fourierdlem89 46116 fourierdlem90 46117 fourierdlem91 46118 fourierdlem104 46131 |
Copyright terms: Public domain | W3C validator |