![]() |
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 648 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒) |
3 | 2 | anabss7 672 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: anabss3 674 anandirs 678 fvreseq 7037 funcestrcsetclem7 18094 funcsetcestrclem7 18109 lmodvsdi 20483 lmodvsdir 20484 lmodvsass 20485 lss0cl 20545 phlpropd 21192 chpdmatlem3 22324 mbfimasn 25131 slmdvsdi 32338 slmdvsdir 32339 slmdvsass 32340 metider 32812 funcringcsetcALTV2lem7 46842 funcringcsetclem7ALTV 46865 |
Copyright terms: Public domain | W3C validator |