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 485 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
2 | adantr2.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylanr1 680 | 1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜏) ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: smoord 8002 addsrmo 10495 mulsrmo 10496 lediv12a 11533 nrmmetd 23184 pntrmax 26140 ablo4 28327 mdslmd3i 30109 atom1d 30130 fsumiunle 30545 esumiun 31353 poimirlem28 34935 fdc 35035 incsequz 35038 crngm4 35296 ps-2 36629 aacllem 44922 |
Copyright terms: Public domain | W3C validator |