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 487 | . 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑) | |
2 | adantl2.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylanl1 678 | 1 ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 399 |
This theorem is referenced by: ad4ant23 751 ad4ant24 752 ad4ant234 1170 fiunlem 7635 sbthlem8 8626 caucvgb 15028 metustto 23155 grpoidinvlem3 28275 nmoub3i 28542 riesz3i 29831 csmdsymi 30103 finxpreclem3 34666 fin2so 34871 matunitlindflem1 34880 mblfinlem2 34922 mblfinlem3 34923 ismblfin 34925 itg2addnclem 34935 ftc1anclem7 34965 ftc1anc 34967 fzmul 35008 fdc 35012 incsequz2 35016 isbnd3 35054 bndss 35056 ismtyres 35078 rngoisocnv 35251 xralrple2 41612 xralrple3 41632 limsupmnflem 41991 climrescn 42019 xlimliminflimsup 42133 dirkertrigeq 42377 fourierdlem12 42395 fourierdlem50 42432 fourierdlem103 42485 fourierdlem104 42486 etransclem35 42545 sge0iunmptlemfi 42686 iundjiun 42733 meaiininclem 42759 hoidmvle 42873 ovnhoilem2 42875 smflimlem1 43038 smfrec 43055 smfliminflem 43095 |
Copyright terms: Public domain | W3C validator |