![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adant2r | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
Ref | Expression |
---|---|
ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant2r | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 481 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an2 1161 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: ltdiv23 12157 lediv23 12158 divalglem8 16402 isdrngd 20743 isdrngdOLD 20745 deg1tm 26146 ax5seglem1 28862 ax5seglem2 28863 nvaddsub4 30590 nmoub2i 30707 cdleme21at 40027 cdleme42f 40179 trlcoabs2N 40421 tendoplcl2 40477 tendopltp 40479 cdlemk2 40531 cdlemk8 40537 cdlemk9 40538 cdlemk9bN 40539 cdleml8 40682 dihglblem3N 40994 dihglblem3aN 40995 fourierdlem42 45770 lincscm 47813 itsclc0yqsol 48152 |
Copyright terms: Public domain | W3C validator |