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 399 |
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 210 df-an 400 |
This theorem is referenced by: anabss3 675 anandirs 679 fvreseq 6838 funcestrcsetclem7 17607 funcsetcestrclem7 17622 lmodvsdi 19876 lmodvsdir 19877 lmodvsass 19878 lss0cl 19937 phlpropd 20571 chpdmatlem3 21691 mbfimasn 24483 slmdvsdi 31141 slmdvsdir 31142 slmdvsass 31143 metider 31512 funcringcsetcALTV2lem7 45216 funcringcsetclem7ALTV 45239 |
Copyright terms: Public domain | W3C validator |