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 488 | . 2 ⊢ ((𝜏 ∧ 𝜒) → 𝜒) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an3 1167 | 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: wfrlem12 8063 ecopovtrn 8499 rrxmet 24302 nvaddsub4 28735 adjlnop 30164 pl1cn 31616 rrnmet 35722 lflsub 36816 lflmul 36817 cvlatexch3 37087 cdleme5 37989 cdlemeg46rjgN 38271 cdlemg2l 38352 cdlemg10c 38388 tendospcanN 38772 dicvaddcl 38939 dicvscacl 38940 dochexmidlem8 39216 limsupre3lem 42946 fourierdlem42 43363 fourierdlem113 43433 ovnsupge0 43768 ovncvrrp 43775 ovnhoilem2 43813 |
Copyright terms: Public domain | W3C validator |