![]() |
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 10261 axdc3lem4 10444 issubmnd 18648 mhmima 18702 maducoeval2 22124 cramerlem3 22173 restnlly 22968 efgh 26032 hasheuni 33021 matunitlindflem1 36422 pellex 41506 mendlmod 41868 disjf1o 43822 ssfiunibd 43954 mullimc 44267 mullimcf 44274 limclner 44302 limsupresxr 44417 liminfresxr 44418 sge0lefi 45049 isomenndlem 45181 hoicvr 45199 ovncvrrp 45215 rhmimasubrng 46678 |
Copyright terms: Public domain | W3C validator |