![]() |
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 485 | . 2 ⊢ ((𝜏 ∧ 𝜒) → 𝜒) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an3 1165 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: wfrlem12OLD 8265 ecopovtrn 8758 rrxmet 24770 nvaddsub4 29546 adjlnop 30975 pl1cn 32476 rrnmet 36278 lflsub 37519 lflmul 37520 cvlatexch3 37790 cdleme5 38693 cdlemeg46rjgN 38975 cdlemg2l 39056 cdlemg10c 39092 tendospcanN 39476 dicvaddcl 39643 dicvscacl 39644 dochexmidlem8 39920 limsupre3lem 43944 fourierdlem42 44361 fourierdlem113 44431 ovnsupge0 44769 ovncvrrp 44776 ovnhoilem2 44814 |
Copyright terms: Public domain | W3C validator |