| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > adantrlr | Structured version Visualization version GIF version | ||
| Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
| Ref | Expression |
|---|---|
| adantr2.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
| Ref | Expression |
|---|---|
| adantrlr | ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜏) ∧ 𝜒)) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl 482 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
| 2 | adantr2.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 3 | 1, 2 | sylanr1 682 | 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: smoord 8405 addsrmo 11113 mulsrmo 11114 lediv12a 12161 nrmmetd 24587 pntrmax 27608 ablo4 30569 mdslmd3i 32351 atom1d 32372 fsumiunle 32831 esumiun 34095 poimirlem28 37655 fdc 37752 incsequz 37755 crngm4 38010 ps-2 39480 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |