| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3adant3l | 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 |
|---|---|
| 3adant3l | ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpr 484 | . 2 ⊢ ((𝜏 ∧ 𝜒) → 𝜒) | |
| 2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 3 | 1, 2 | syl3an3 1166 | 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: wfrlem12OLD 8360 ecopovtrn 8860 rrxmet 25442 nvaddsub4 30676 adjlnop 32105 pl1cn 33954 rrnmet 37836 lflsub 39068 lflmul 39069 cvlatexch3 39339 cdleme5 40242 cdlemeg46rjgN 40524 cdlemg2l 40605 cdlemg10c 40641 tendospcanN 41025 dicvaddcl 41192 dicvscacl 41193 dochexmidlem8 41469 limsupre3lem 45747 fourierdlem42 46164 fourierdlem113 46234 ovnsupge0 46572 ovncvrrp 46579 ovnhoilem2 46617 |
| Copyright terms: Public domain | W3C validator |