![]() |
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 486 | . 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an1 1164 | 1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: ad5ant245 1362 cfsmolem 10214 axdc3lem4 10397 issubmnd 18591 maducoeval2 22012 cramerlem3 22061 restnlly 22856 efgh 25920 hasheuni 32748 matunitlindflem1 36124 pellex 41205 mendlmod 41567 disjf1o 43502 ssfiunibd 43634 mullimc 43947 mullimcf 43954 limclner 43982 limsupresxr 44097 liminfresxr 44098 sge0lefi 44729 isomenndlem 44861 hoicvr 44879 ovncvrrp 44895 |
Copyright terms: Public domain | W3C validator |