| 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 18191 funcsetcestrclem7 18206 lmodvsdi 20883 lmodvsdir 20884 lmodvsass 20885 lss0cl 20945 phlpropd 21673 chpdmatlem3 22846 mbfimasn 25667 slmdvsdi 33221 slmdvsdir 33222 slmdvsass 33223 metider 33893 funcringcsetcALTV2lem7 48212 funcringcsetclem7ALTV 48235 |
| Copyright terms: Public domain | W3C validator |