![]() |
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 649 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒) |
3 | 2 | anabss7 673 | 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: anabss3 675 anandirs 679 fvreseq 7060 funcestrcsetclem7 18202 funcsetcestrclem7 18217 lmodvsdi 20900 lmodvsdir 20901 lmodvsass 20902 lss0cl 20963 phlpropd 21691 chpdmatlem3 22862 mbfimasn 25681 slmdvsdi 33204 slmdvsdir 33205 slmdvsass 33206 metider 33855 funcringcsetcALTV2lem7 48140 funcringcsetclem7ALTV 48163 |
Copyright terms: Public domain | W3C validator |