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 715 | . 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓)) |
3 | adantl3r.1 | . 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | sylanl1 680 | 1 ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 |
This theorem is referenced by: adantl4r 755 iscgrglt 26605 legov 26676 dfcgra2 26921 suppovss 30737 cyc3genpm 31138 rhmimaidl 31323 fedgmul 31426 zarclsun 31534 omssubadd 31979 circlemeth 32332 poimirlem29 35543 adantlllr 42256 supxrge 42550 xrralrecnnle 42595 rexabslelem 42631 limclner 42867 xlimmnfvlem2 43049 xlimmnfv 43050 xlimpnfvlem2 43053 xlimpnfv 43054 climxlim2lem 43061 icccncfext 43103 fourierdlem64 43386 fourierdlem73 43395 etransclem35 43485 sge0tsms 43593 hoicvr 43761 hspmbllem2 43840 smflimlem2 43979 smflimlem4 43981 |
Copyright terms: Public domain | W3C validator |