![]() |
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 486 | . 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑) | |
2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylanl1 679 | 1 ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: ad4ant23 752 ad4ant24 753 ad4ant234 1176 fiunlem 7875 sbthlem8 9035 caucvgb 15565 metustto 23912 grpoidinvlem3 29451 nmoub3i 29718 riesz3i 31007 csmdsymi 31279 finxpreclem3 35867 fin2so 36068 matunitlindflem1 36077 mblfinlem2 36119 mblfinlem3 36120 ismblfin 36122 itg2addnclem 36132 ftc1anclem7 36160 ftc1anc 36162 fzmul 36203 fdc 36207 incsequz2 36211 isbnd3 36246 bndss 36248 ismtyres 36270 rngoisocnv 36443 xralrple2 43595 xralrple3 43615 cvgcaule 43734 limsupmnflem 43968 climrescn 43996 xlimliminflimsup 44110 dirkertrigeq 44349 fourierdlem12 44367 fourierdlem50 44404 fourierdlem103 44457 fourierdlem104 44458 etransclem35 44517 sge0iunmptlemfi 44661 iundjiun 44708 meaiininclem 44734 hoidmvle 44848 ovnhoilem2 44850 smflimlem1 45019 smfrec 45037 smfliminflem 45078 |
Copyright terms: Public domain | W3C validator |