![]() |
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 481 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
2 | adantr2.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylanr1 680 | 1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜏) ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: smoord 8395 addsrmo 11116 mulsrmo 11117 lediv12a 12159 nrmmetd 24574 pntrmax 27593 ablo4 30483 mdslmd3i 32265 atom1d 32286 fsumiunle 32730 esumiun 33927 poimirlem28 37349 fdc 37446 incsequz 37449 crngm4 37704 ps-2 39177 aacllem 48549 |
Copyright terms: Public domain | W3C validator |