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 488 | . 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an1 1165 | 1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: ad5ant245 1363 cfsmolem 9881 axdc3lem4 10064 issubmnd 18197 maducoeval2 21534 cramerlem3 21583 restnlly 22376 efgh 25427 hasheuni 31762 matunitlindflem1 35508 pellex 40358 mendlmod 40719 disjf1o 42400 ssfiunibd 42519 mullimc 42830 mullimcf 42837 limclner 42865 limsupresxr 42980 liminfresxr 42981 sge0lefi 43609 isomenndlem 43741 hoicvr 43759 ovncvrrp 43775 |
Copyright terms: Public domain | W3C validator |