![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adant1l | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
Ref | Expression |
---|---|
ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant1l | ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 483 | . 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an1 1161 | 1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1085 |
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 df-3an 1087 |
This theorem is referenced by: ad5ant245 1359 cfsmolem 10267 axdc3lem4 10450 issubmnd 18686 mhmima 18742 rhmimasubrng 20454 maducoeval2 22362 cramerlem3 22411 restnlly 23206 efgh 26286 hasheuni 33381 matunitlindflem1 36787 pellex 41875 mendlmod 42237 disjf1o 44188 ssfiunibd 44317 mullimc 44630 mullimcf 44637 limclner 44665 limsupresxr 44780 liminfresxr 44781 sge0lefi 45412 isomenndlem 45544 hoicvr 45562 ovncvrrp 45578 |
Copyright terms: Public domain | W3C validator |