| 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 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: adantl4r 755 iscgrglt 28522 legov 28593 dfcgra2 28838 suppovss 32690 cyc3genpm 33172 elrgspnlem4 33249 rhmimaidl 33460 fedgmul 33682 zarclsun 33869 omssubadd 34302 circlemeth 34655 poimirlem29 37656 adantlllr 45044 supxrge 45349 xrralrecnnle 45394 rexabslelem 45429 limclner 45666 xlimmnfvlem2 45848 xlimmnfv 45849 xlimpnfvlem2 45852 xlimpnfv 45853 climxlim2lem 45860 icccncfext 45902 fourierdlem64 46185 fourierdlem73 46194 etransclem35 46284 sge0tsms 46395 hoicvr 46563 hspmbllem2 46642 smflimlem2 46787 smflimlem4 46789 |
| Copyright terms: Public domain | W3C validator |