![]() |
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 483 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
2 | adantr2.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylanr1 680 | 1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜏) ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 397 |
This theorem is referenced by: smoord 8311 addsrmo 11009 mulsrmo 11010 lediv12a 12048 nrmmetd 23930 pntrmax 26912 ablo4 29492 mdslmd3i 31274 atom1d 31295 fsumiunle 31725 esumiun 32693 poimirlem28 36106 fdc 36204 incsequz 36207 crngm4 36462 ps-2 37941 aacllem 47238 |
Copyright terms: Public domain | W3C validator |