![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > adantlll | Structured version Visualization version Unicode 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 467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | adantl2.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylanl1 660 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 df-an 377 |
This theorem is referenced by: fun11iun 6779 oewordri 7318 sbthlem8 7714 xmulass 11601 caucvgb 13794 clsnsg 21172 metustto 21616 constr3cycl 25437 grpoidinvlem3 25982 nmoub3i 26462 riesz3i 27763 csmdsymi 28035 finxpreclem3 31829 fin2so 31976 mblfinlem2 32022 mblfinlem3 32023 ismblfin 32025 itg2addnclem 32037 ftc1anclem7 32067 ftc1anc 32069 fzmul 32113 fdc 32118 incsequz2 32122 isbnd3 32160 bndss 32162 ismtyres 32184 rngoisocnv 32264 xralrple2 37614 dirkertrigeq 38000 fourierdlem12 38018 fourierdlem50 38057 fourierdlem103 38110 fourierdlem104 38111 etransclem35 38171 sge0iunmptlemfi 38292 iundjiun 38335 hoidmvle 38459 ovnhoilem2 38461 |
Copyright terms: Public domain | W3C validator |