![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anabsan2 | Structured version Visualization version GIF version |
Description: Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.) |
Ref | Expression |
---|---|
anabsan2.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜓)) → 𝜒) |
Ref | Expression |
---|---|
anabsan2 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anabsan2.1 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜓)) → 𝜒) | |
2 | 1 | an12s 860 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒) |
3 | 2 | anabss7 879 | 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 197 df-an 385 |
This theorem is referenced by: anabss3 881 anandirs 891 fvreseq 6359 funcestrcsetclem7 16833 funcsetcestrclem7 16848 lmodvsdi 18934 lmodvsdir 18935 lmodvsass 18936 lss0cl 18995 phlpropd 20048 chpdmatlem3 20693 mbfimasn 23446 slmdvsdi 29896 slmdvsdir 29897 slmdvsass 29898 metider 30065 funcringcsetcALTV2lem7 42367 funcringcsetclem7ALTV 42390 |
Copyright terms: Public domain | W3C validator |