| 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 1189 fiunlem 7923 sbthlem8 9066 caucvgb 15707 metustto 24610 grpoidinvlem3 30706 nmoub3i 30973 riesz3i 32262 csmdsymi 32534 finxpreclem3 37884 fin2so 38103 matunitlindflem1 38112 mblfinlem2 38154 mblfinlem3 38155 ismblfin 38157 itg2addnclem 38167 ftc1anclem7 38195 ftc1anc 38197 fzmul 38237 fdc 38241 incsequz2 38245 isbnd3 38280 bndss 38282 ismtyres 38304 rngoisocnv 38477 xralrple2 45927 xralrple3 45946 cvgcaule 46062 limsupmnflem 46291 climrescn 46319 xlimliminflimsup 46433 dirkertrigeq 46672 fourierdlem12 46690 fourierdlem50 46727 fourierdlem103 46780 fourierdlem104 46781 etransclem35 46840 sge0iunmptlemfi 46984 iundjiun 47031 meaiininclem 47057 hoidmvle 47171 ovnhoilem2 47173 smflimlem1 47342 smfrec 47360 smfliminflem 47401 |
| Copyright terms: Public domain | W3C validator |