> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/300-logic/310-mathematical-logic/monotonicity-of-entailment.md).

# Monotonicity of entailment

When a sequent `p |- p` is ∧I with a sequent `q |- q`, their antecedents will be united (set union), while the consequnt becomes the conjunction of `p ∧ q`, so the resulting sequent is `p, q |- p ∧ q`.

Now, if we immediately eliminate the right conjunct `q` from that sequent, the resulting sequent's conclusion will contain just `p` but its antecedent will still contain `q`'s premises: `p, q |- p`

```javascript
------ AS¹   -------- AS²
p |- p        q |- q
--------------------- ∧I
    p, q |- p ∧ q
--------------------- ∧Eʟ
    p, q |- p
```