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 712 | . 2 ⊢ (((𝜑 ∧ 𝜂) ∧ 𝜓) → (𝜑 ∧ 𝜓)) |
3 | adantl3r.1 | . 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | sylanl1 677 | 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 206 df-an 397 |
This theorem is referenced by: adantl4r 752 iscgrglt 26875 legov 26946 dfcgra2 27191 suppovss 31017 cyc3genpm 31419 rhmimaidl 31609 fedgmul 31712 zarclsun 31820 omssubadd 32267 circlemeth 32620 poimirlem29 35806 adantlllr 42583 supxrge 42877 xrralrecnnle 42922 rexabslelem 42958 limclner 43192 xlimmnfvlem2 43374 xlimmnfv 43375 xlimpnfvlem2 43378 xlimpnfv 43379 climxlim2lem 43386 icccncfext 43428 fourierdlem64 43711 fourierdlem73 43720 etransclem35 43810 sge0tsms 43918 hoicvr 44086 hspmbllem2 44165 smflimlem2 44307 smflimlem4 44309 |
Copyright terms: Public domain | W3C validator |