| 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 484 | . 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑) | |
| 2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 3 | 1, 2 | syl3an1 1164 | 1 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: ad5ant245 1363 cfsmolem 10310 axdc3lem4 10493 issubmnd 18774 mhmima 18838 rhmimasubrng 20566 maducoeval2 22646 cramerlem3 22695 restnlly 23490 efgh 26583 hasheuni 34086 matunitlindflem1 37623 pellex 42846 mendlmod 43201 disjf1o 45196 ssfiunibd 45321 mullimc 45631 mullimcf 45638 limclner 45666 limsupresxr 45781 liminfresxr 45782 sge0lefi 46413 isomenndlem 46545 hoicvr 46563 ovncvrrp 46579 |
| Copyright terms: Public domain | W3C validator |