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 487 | . 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an1 1159 | 1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 df-3an 1085 |
This theorem is referenced by: ad5ant245 1357 cfsmolem 9686 axdc3lem4 9869 issubmnd 17932 maducoeval2 21243 cramerlem3 21292 restnlly 22084 efgh 25119 hasheuni 31339 matunitlindflem1 34882 pellex 39425 mendlmod 39786 disjf1o 41444 ssfiunibd 41568 mullimc 41889 mullimcf 41896 limclner 41924 limsupresxr 42039 liminfresxr 42040 sge0lefi 42673 isomenndlem 42805 hoicvr 42823 ovncvrrp 42839 |
Copyright terms: Public domain | W3C validator |