| 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 488 | . 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑) | |
| 2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
| 3 | 1, 2 | sylanl1 690 | 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 209 df-an 400 |
| This theorem is referenced by: ad4ant23 763 ad4ant24 764 ad4ant234 1188 fiunlem 7918 sbthlem8 9060 caucvgb 15698 metustto 24601 grpoidinvlem3 30666 nmoub3i 30933 riesz3i 32222 csmdsymi 32494 finxpreclem3 37848 fin2so 38067 matunitlindflem1 38076 mblfinlem2 38118 mblfinlem3 38119 ismblfin 38121 itg2addnclem 38131 ftc1anclem7 38159 ftc1anc 38161 fzmul 38201 fdc 38205 incsequz2 38209 isbnd3 38244 bndss 38246 ismtyres 38268 rngoisocnv 38441 xralrple2 45891 xralrple3 45910 cvgcaule 46026 limsupmnflem 46255 climrescn 46283 xlimliminflimsup 46397 dirkertrigeq 46636 fourierdlem12 46654 fourierdlem50 46691 fourierdlem103 46744 fourierdlem104 46745 etransclem35 46804 sge0iunmptlemfi 46948 iundjiun 46995 meaiininclem 47021 hoidmvle 47135 ovnhoilem2 47137 smflimlem1 47306 smfrec 47324 smfliminflem 47365 |
| Copyright terms: Public domain | W3C validator |