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 645 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒) |
3 | 2 | anabss7 669 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: anabss3 671 anandirs 675 fvreseq 6802 funcestrcsetclem7 17384 funcsetcestrclem7 17399 lmodvsdi 19586 lmodvsdir 19587 lmodvsass 19588 lss0cl 19647 phlpropd 20727 chpdmatlem3 21376 mbfimasn 24160 slmdvsdi 30770 slmdvsdir 30771 slmdvsass 30772 metider 31033 funcringcsetcALTV2lem7 44241 funcringcsetclem7ALTV 44264 |
Copyright terms: Public domain | W3C validator |