| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > adantrrr | 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 |
|---|---|
| adantrrr | ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜏))) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl 482 | . 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒) | |
| 2 | adantr2.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 3 | 1, 2 | sylanr2 683 | 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: zorn2lem6 10541 addsrmo 11113 mulsrmo 11114 lemul12b 12124 lt2mul2div 12146 lediv12a 12161 tgcl 22976 neissex 23135 alexsublem 24052 alexsubALTlem4 24058 iscmet3 25327 mulsuniflem 28175 ablo4 30569 shscli 31336 mdslmd3i 32351 brab2d 32619 cvmliftmolem2 35287 mblfinlem4 37667 heibor 37828 ablo4pnp 37887 crngm4 38010 cvratlem 39423 ps-2 39480 cdlemftr3 40567 mzpcompact2lem 42762 |
| Copyright terms: Public domain | W3C validator |