![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > adantl3r | Structured version Visualization version GIF version |
Description: Deduction adding 1 conjunct to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
Ref | Expression |
---|---|
adantl3r.1 | ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
adantl3r | ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
2 | 1 | adantlr 711 | . 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓)) |
3 | adantl3r.1 | . 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | sylanl1 676 | 1 ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: adantl4r 751 iscgrglt 25987 legov 26058 dfcgra2 26303 suppovss 30121 cyc3genpm 30437 fedgmul 30636 omssubadd 31180 circlemeth 31533 poimirlem29 34477 adantlllr 40861 supxrge 41172 xrralrecnnle 41219 rexabslelem 41259 limclner 41499 xlimmnfvlem2 41681 xlimmnfv 41682 xlimpnfvlem2 41685 xlimpnfv 41686 climxlim2lem 41693 icccncfext 41737 fourierdlem64 42023 fourierdlem73 42032 etransclem35 42122 sge0tsms 42230 hoicvr 42398 hspmbllem2 42477 smflimlem2 42616 smflimlem4 42618 |
Copyright terms: Public domain | W3C validator |