| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > adantlll | Structured version Visualization version GIF version | ||
| Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.) |
| Ref | Expression |
|---|---|
| adantl2.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| adantlll | ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpr 484 | . 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑) | |
| 2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
| 3 | 1, 2 | 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: ad4ant23 753 ad4ant24 754 ad4ant234 1176 fiunlem 7966 sbthlem8 9130 caucvgb 15716 metustto 24566 grpoidinvlem3 30525 nmoub3i 30792 riesz3i 32081 csmdsymi 32353 finxpreclem3 37394 fin2so 37614 matunitlindflem1 37623 mblfinlem2 37665 mblfinlem3 37666 ismblfin 37668 itg2addnclem 37678 ftc1anclem7 37706 ftc1anc 37708 fzmul 37748 fdc 37752 incsequz2 37756 isbnd3 37791 bndss 37793 ismtyres 37815 rngoisocnv 37988 xralrple2 45365 xralrple3 45385 cvgcaule 45502 limsupmnflem 45735 climrescn 45763 xlimliminflimsup 45877 dirkertrigeq 46116 fourierdlem12 46134 fourierdlem50 46171 fourierdlem103 46224 fourierdlem104 46225 etransclem35 46284 sge0iunmptlemfi 46428 iundjiun 46475 meaiininclem 46501 hoidmvle 46615 ovnhoilem2 46617 smflimlem1 46786 smfrec 46804 smfliminflem 46845 |
| Copyright terms: Public domain | W3C validator |